diff --git a/model_with_structures/model.typ b/model_with_structures/model.typ
index 8d61739..42d7b14 100644
--- a/model_with_structures/model.typ
+++ b/model_with_structures/model.typ
@@ -758,7 +758,7 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ modify final value: unit],
+    name: [ modify final value],
 
     $cl cdl v_m, v_r, v_w cdr, mu cr
      xarrowSquiggly(cl \# . \, a cr)_modify
@@ -768,32 +768,6 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
 
 #h(10pt)
 
-#align(center, prooftree(
-  vertical-spacing: 4pt,
-  rule(
-    name: [ modify final value: ref],
-
-    $cl mu[l], mu cr xarrowSquiggly(cl \# . \, a cr)_modify cl v', mu' cr$,
-    $cl rf l, mu cr xarrowSquiggly(cl \# . \, a cr)_modify cl rf l, mu'[l <- v'] cr$,
-  )
-))
-
-#h(10pt)
-
-#align(center, prooftree(
-  vertical-spacing: 4pt,
-  rule(
-    name: [ modify final value: tuple],
-
-    $cl v_1, mu_0 cr xarrowSquiggly(cl \# . \, a cr)_modify cl v'_1, mu_1, cr$,
-    $...$,
-    $cl v_n, mu_(n - 1) cr xarrowSquiggly(cl \# . \, a cr)_modify cl v'_n, mu_n, cr$,
-    $cl [v_1, ... v_n], mu cr xarrowSquiggly(cl \# . \, a cr)_modify cl [v'_1, ... v'_n], mu_n cr$,
-  )
-))
-
-#h(10pt)
-
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
@@ -811,7 +785,7 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
   rule(
     name: [ modify tuple value],
 
-    $cl v_i, mu cr xarrowSquiggly(cl pi \, a cr)_modify cl v'_i, mu', cr$,
+    $cl v_i, mu cr xarrowSquiggly(cl p \, a cr)_modify cl v'_i, mu', cr$,
     $cl [v_1, ... v_i, ... v_n], mu cr xarrowSquiggly(cl i.pi \, a cr)_modify cl [v_1, ... v'_i, ... v_n], mu' cr$,
   )
 ))
@@ -1411,7 +1385,7 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
   rule(
     name: [ lambda check],
 
-    $mu ttags lambda space overline(s) : lambda overline(t)$,
+    $mu ttags lambda space overline(s) :$,
   )
 ))
 #align(center, prooftree(
@@ -1444,7 +1418,6 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
     // TODO: FIXME: introduce global types and vals
     $types_0 = types_#[glob]$,
     $vals_0 = vals_#[glob]$,
-    $mu_0 = mu$,
 
     // NOTE: dashed arrow to fill context
     $cl types_0, vals_0,  mu_0 cr
@@ -1599,31 +1572,4 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
   )
 ))
 
-=== Program Evaluation
-
-#let progeval = `prog eval`
-
-#align(center, prooftree(
-  vertical-spacing: 4pt,
-  rule(
-    name: [ program evaluation],
-
-    // NOTE: expr type expected to ~ match t (maybe except some automaticc modifiers)
-    // expect well typed program
-
-    $cl types_0, vals_0, mu_0 cr xarrowSquiggly(d_1)_init cl types_1, vals_1, mu_1 cr$,
-    $...$,
-    $cl types_(n - 1), vals_(n - 1), mu_(n - 1) cr xarrowSquiggly(d_n)_init cl types_n, vals_n, mu_n cr$,
-
-    // TODO: FIXME: some easy way to pass to eval ??
-    $types_#[glob] = types_n$,
-    $vals_#[glob] = vals_n$,
-    $mu_#[glob] = mu_n$,
-
-    $cl types_n, vals_n, mu_n cr xarrow(s) cl types', vals', mu' cr$,
-
-    $cl types_0, vals_0, mu_0 cr xarrowSquiggly(d_1 ... d_n s)_prog_eval  cl types', vals', mu' cr$
-  )
-))
-
 ]