diff --git a/graphs/dependency.dot b/graphs/dependency.dot
index 4a3e429..2b856c8 100644
--- a/graphs/dependency.dot
+++ b/graphs/dependency.dot
@@ -37,6 +37,18 @@ digraph theorem_deps {
   red1r_fv [label="red1r_fv", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="red1r_fv theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
   lemma_2_1_fv_preserved [label="lemma_2_1_fv_preserved", color="#38761d", fillcolor="#d9ead3", style="rounded,filled", fontcolor="#222222", tooltip="lemma_2_1_fv_preserved (section 2.1) theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=box];
   lemma_2_3_beta_sim [label="lemma_2_3_beta_sim", color="#38761d", fillcolor="#d9ead3", style="rounded,filled", fontcolor="#222222", tooltip="lemma_2_3_beta_sim (section 2.3) theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=box];
+  par_red1_iff [label="par_red1_iff", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="par_red1_iff theory/Parallel.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  red1_in_par [label="red1_in_par", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="red1_in_par theory/Parallel.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  par_context [label="par_context", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="par_context theory/Parallel.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  par_to_red1_or_eq [label="par_to_red1_or_eq", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="par_to_red1_or_eq theory/Parallel.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  red1_or_eq_to_par [label="red1_or_eq_to_par", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="red1_or_eq_to_par theory/Parallel.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  par_reflexive [label="par_reflexive", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="par_reflexive theory/Parallel.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  gen_list_length [label="gen_list_length", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="gen_list_length theory/Random.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  check_term_true [label="check_term_true", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="check_term_true theory/Random.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  check_all_true [label="check_all_true", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="check_all_true theory/Random.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  gen_sound [label="gen_sound", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="gen_sound theory/Random.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  gen_complete [label="gen_complete", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="gen_complete theory/Random.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  gen_fv_preserved [label="gen_fv_preserved", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="gen_fv_preserved theory/Random.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
   zdecs_sound [label="zdecs_sound", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="zdecs_sound theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
   zdecs_complete [label="zdecs_complete", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="zdecs_complete theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
   positions_at [label="positions_at", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="positions_at theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
@@ -53,6 +65,26 @@ digraph theorem_deps {
   has_red_f [label="has_red_f", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="has_red_f theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
   has_red_spec [label="has_red_spec", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="has_red_spec theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
   red1_dec [label="red1_dec", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="red1_dec theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  open_rec_app [label="open_rec_app", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="open_rec_app theory/Substitution.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  open_rec_lam [label="open_rec_lam", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="open_rec_lam theory/Substitution.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  open_rec_esub [label="open_rec_esub", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="open_rec_esub theory/Substitution.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  close_rec_app [label="close_rec_app", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="close_rec_app theory/Substitution.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  close_rec_lam [label="close_rec_lam", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="close_rec_lam theory/Substitution.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  close_rec_esub [label="close_rec_esub", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="close_rec_esub theory/Substitution.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  subst_app [label="subst_app", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="subst_app theory/Substitution.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  subst_lam [label="subst_lam", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="subst_lam theory/Substitution.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  subst_esub [label="subst_esub", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="subst_esub theory/Substitution.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  subst_notin [label="subst_notin", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="subst_notin theory/Substitution.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  subst_lc_self [label="subst_lc_self", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="subst_lc_self theory/Substitution.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  subst_other [label="subst_other", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="subst_other theory/Substitution.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  red_sub_root_to_red1 [label="red_sub_root_to_red1", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="red_sub_root_to_red1 theory/Subsystem.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  red_sub_to_red1 [label="red_sub_to_red1", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="red_sub_to_red1 theory/Subsystem.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  red_sub_context [label="red_sub_context", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="red_sub_context theory/Subsystem.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  red_sub_gc [label="red_sub_gc", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="red_sub_gc theory/Subsystem.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  red_sub_r [label="red_sub_r", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="red_sub_r theory/Subsystem.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  occurs_zfill [label="occurs_zfill", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="occurs_zfill theory/Subsystem.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  zfill_occurs0 [label="zfill_occurs0", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="zfill_occurs0 theory/Subsystem.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  R_Gc_disjoint [label="R_Gc_disjoint", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="R_Gc_disjoint theory/Subsystem.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
   corpus_sound [label="corpus_sound", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="corpus_sound theory/Tests.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
   corpus_complete [label="corpus_complete", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="corpus_complete theory/Tests.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
   corpus_decides [label="corpus_decides", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="corpus_decides theory/Tests.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
@@ -84,6 +116,15 @@ digraph theorem_deps {
   red1r_fv -> lemma_2_1_fv_preserved;
   Plus_red1_context -> lemma_2_3_beta_sim;
   lemma_2_2_full_comp -> lemma_2_3_beta_sim;
+  par_red1_iff -> par_to_red1_or_eq;
+  par_red1_iff -> red1_or_eq_to_par;
+  has_red_spec -> check_term_true;
+  steps_sound_red1 -> check_term_true;
+  check_term_true -> check_all_true;
+  steps_sound -> gen_sound;
+  steps_complete -> gen_complete;
+  lemma_2_1_fv_preserved -> gen_fv_preserved;
+  steps_sound_red1 -> gen_fv_preserved;
   zdecs_sound -> root_steps_sound;
   zdecs_complete -> root_steps_complete;
   positions_at -> steps_sound;
@@ -99,6 +140,13 @@ digraph theorem_deps {
   steps_complete -> has_red_spec;
   steps_sound -> has_red_spec;
   has_red_spec -> red1_dec;
+  close_rec_notin -> subst_notin;
+  open_rec_occurs_false -> subst_notin;
+  subst_fvar_self -> subst_lc_self;
+  subst_fvar_other -> subst_other;
+  red_sub_root_to_red1 -> red_sub_to_red1;
+  occurs_zfill -> zfill_occurs0;
+  zfill_occurs0 -> R_Gc_disjoint;
   steps_sound -> corpus_sound;
   steps_complete -> corpus_complete;
   has_red_spec -> corpus_decides;
diff --git a/graphs/dependency.png b/graphs/dependency.png
index d0955f3..b319001 100644
Binary files a/graphs/dependency.png and b/graphs/dependency.png differ
diff --git a/graphs/dependency.svg b/graphs/dependency.svg
index a8e5d14..ca398b7 100644
--- a/graphs/dependency.svg
+++ b/graphs/dependency.svg
@@ -4,25 +4,25 @@
 <!-- Generated by graphviz version 2.42.4 (0)
  -->
 <!-- Title: theorem_deps Pages: 1 -->
-<svg width="953pt" height="930pt"
- viewBox="0.00 0.00 953.29 930.00" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink">
-<g id="graph0" class="graph" transform="scale(1 1) rotate(0) translate(4 926)">
+<svg width="1085pt" height="1875pt"
+ viewBox="0.00 0.00 1085.21 1875.00" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink">
+<g id="graph0" class="graph" transform="scale(1 1) rotate(0) translate(4 1871)">
 <title>theorem_deps</title>
-<polygon fill="white" stroke="transparent" points="-4,4 -4,-926 949.29,-926 949.29,4 -4,4"/>
-<text text-anchor="start" x="236.65" y="-909.4" font-family="Inter" font-weight="bold" font-size="12.00">Milner&#39;s Lambda&#45;Calculus with Partial Substitutions &#45; theorem dependency (M2)</text>
-<text text-anchor="start" x="399.65" y="-899.8" font-family="Inter" font-size="9.00" fill="#38761d">proved</text>
-<text text-anchor="start" x="429.65" y="-899.8" font-family="Inter" font-size="9.00"> &#160;&#160;</text>
-<text text-anchor="start" x="436.65" y="-899.8" font-family="Inter" font-size="9.00" fill="#b45f06">stated</text>
-<text text-anchor="start" x="463.65" y="-899.8" font-family="Inter" font-size="9.00"> &#160;&#160;</text>
-<text text-anchor="start" x="470.65" y="-899.8" font-family="Inter" font-size="9.00" fill="#777777">planned</text>
-<text text-anchor="start" x="504.65" y="-899.8" font-family="Inter" font-size="9.00"> &#160;&#160;</text>
-<text text-anchor="start" x="511.65" y="-899.8" font-family="Inter" font-size="9.00" fill="#cc0000">blocked</text>
+<polygon fill="white" stroke="transparent" points="-4,4 -4,-1871 1081.21,-1871 1081.21,4 -4,4"/>
+<text text-anchor="start" x="302.6" y="-1854.4" font-family="Inter" font-weight="bold" font-size="12.00">Milner&#39;s Lambda&#45;Calculus with Partial Substitutions &#45; theorem dependency (M2)</text>
+<text text-anchor="start" x="465.6" y="-1844.8" font-family="Inter" font-size="9.00" fill="#38761d">proved</text>
+<text text-anchor="start" x="495.6" y="-1844.8" font-family="Inter" font-size="9.00"> &#160;&#160;</text>
+<text text-anchor="start" x="502.6" y="-1844.8" font-family="Inter" font-size="9.00" fill="#b45f06">stated</text>
+<text text-anchor="start" x="529.6" y="-1844.8" font-family="Inter" font-size="9.00"> &#160;&#160;</text>
+<text text-anchor="start" x="536.6" y="-1844.8" font-family="Inter" font-size="9.00" fill="#777777">planned</text>
+<text text-anchor="start" x="570.6" y="-1844.8" font-family="Inter" font-size="9.00"> &#160;&#160;</text>
+<text text-anchor="start" x="577.6" y="-1844.8" font-family="Inter" font-size="9.00" fill="#cc0000">blocked</text>
 <!-- fvs_lift -->
 <g id="node1" class="node">
 <title>fvs_lift</title>
 <g id="a_node1"><a xlink:title="fvs_lift theory/Binding.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-563" rx="27" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-560.8" font-family="Inter" font-size="9.00" fill="#222222">fvs_lift</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-650" rx="27" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-647.8" font-family="Inter" font-size="9.00" fill="#222222">fvs_lift</text>
 </a>
 </g>
 </g>
@@ -30,38 +30,38 @@
 <g id="node10" class="node">
 <title>open_rec_fvs</title>
 <g id="a_node10"><a xlink:title="open_rec_fvs theory/Binding.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-615" rx="41.64" ry="18"/>
-<text text-anchor="middle" x="239.88" y="-612.8" font-family="Inter" font-size="9.00" fill="#222222">open_rec_fvs</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-572" rx="41.64" ry="18"/>
+<text text-anchor="middle" x="239.88" y="-569.8" font-family="Inter" font-size="9.00" fill="#222222">open_rec_fvs</text>
 </a>
 </g>
 </g>
 <!-- fvs_lift&#45;&gt;open_rec_fvs -->
 <g id="edge2" class="edge">
 <title>fvs_lift&#45;&gt;open_rec_fvs</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M90.24,-570.23C118.42,-578.72 165.55,-592.91 199.19,-603.04"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="198.95,-605.17 205.3,-604.89 200.16,-601.15 198.95,-605.17"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M87.39,-639.18C108.87,-628.32 143.18,-611.35 173.48,-598 182.74,-593.92 192.85,-589.76 202.3,-586"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="203.27,-587.87 208.08,-583.71 201.72,-583.97 203.27,-587.87"/>
 </g>
 <!-- fvs_zplug_lift -->
 <g id="node25" class="node">
 <title>fvs_zplug_lift</title>
 <g id="a_node25"><a xlink:title="fvs_zplug_lift theory/Metatheory.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-563" rx="40.98" ry="18"/>
-<text text-anchor="middle" x="239.88" y="-560.8" font-family="Inter" font-size="9.00" fill="#222222">fvs_zplug_lift</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-676" rx="40.98" ry="18"/>
+<text text-anchor="middle" x="239.88" y="-673.8" font-family="Inter" font-size="9.00" fill="#222222">fvs_zplug_lift</text>
 </a>
 </g>
 </g>
 <!-- fvs_lift&#45;&gt;fvs_zplug_lift -->
 <g id="edge21" class="edge">
 <title>fvs_lift&#45;&gt;fvs_zplug_lift</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M92.46,-563C118.9,-563 160.28,-563 192.31,-563"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="192.58,-565.1 198.58,-563 192.58,-560.9 192.58,-565.1"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M91.71,-653.84C118.82,-657.92 162.22,-664.45 194.87,-669.37"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="194.59,-671.45 200.84,-670.27 195.22,-667.3 194.59,-671.45"/>
 </g>
 <!-- lift_lc -->
 <g id="node2" class="node">
 <title>lift_lc</title>
 <g id="a_node2"><a xlink:title="lift_lc theory/Binding.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-719" rx="27" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-716.8" font-family="Inter" font-size="9.00" fill="#222222">lift_lc</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-728" rx="27" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-725.8" font-family="Inter" font-size="9.00" fill="#222222">lift_lc</text>
 </a>
 </g>
 </g>
@@ -69,68 +69,68 @@
 <g id="node3" class="node">
 <title>lift_0_lc</title>
 <g id="a_node3"><a xlink:title="lift_0_lc theory/Binding.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-719" rx="27.93" ry="18"/>
-<text text-anchor="middle" x="239.88" y="-716.8" font-family="Inter" font-size="9.00" fill="#222222">lift_0_lc</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-728" rx="27.93" ry="18"/>
+<text text-anchor="middle" x="239.88" y="-725.8" font-family="Inter" font-size="9.00" fill="#222222">lift_0_lc</text>
 </a>
 </g>
 </g>
 <!-- lift_lc&#45;&gt;lift_0_lc -->
 <g id="edge1" class="edge">
 <title>lift_lc&#45;&gt;lift_0_lc</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M92.46,-719C122.79,-719 172.78,-719 205.77,-719"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="206.13,-721.1 212.13,-719 206.13,-716.9 206.13,-721.1"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M92.46,-728C122.79,-728 172.78,-728 205.77,-728"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="206.13,-730.1 212.13,-728 206.13,-725.9 206.13,-730.1"/>
 </g>
 <!-- subst_fvar_self -->
 <g id="node12" class="node">
 <title>subst_fvar_self</title>
 <g id="a_node12"><a xlink:title="subst_fvar_self theory/Binding.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-719" rx="45.72" ry="18"/>
-<text text-anchor="middle" x="408.74" y="-716.8" font-family="Inter" font-size="9.00" fill="#222222">subst_fvar_self</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-728" rx="45.72" ry="18"/>
+<text text-anchor="middle" x="408.74" y="-725.8" font-family="Inter" font-size="9.00" fill="#222222">subst_fvar_self</text>
 </a>
 </g>
 </g>
 <!-- lift_0_lc&#45;&gt;subst_fvar_self -->
 <g id="edge6" class="edge">
 <title>lift_0_lc&#45;&gt;subst_fvar_self</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M267.69,-719C291.68,-719 327.51,-719 356.92,-719"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="357.09,-721.1 363.09,-719 357.09,-716.9 357.09,-721.1"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M267.69,-728C291.68,-728 327.51,-728 356.92,-728"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="357.09,-730.1 363.09,-728 357.09,-725.9 357.09,-730.1"/>
 </g>
 <!-- open_rec_bvar -->
 <g id="node4" class="node">
 <title>open_rec_bvar</title>
 <g id="a_node4"><a xlink:title="open_rec_bvar theory/Binding.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-511" rx="46.38" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-508.8" font-family="Inter" font-size="9.00" fill="#222222">open_rec_bvar</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-520" rx="46.38" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-517.8" font-family="Inter" font-size="9.00" fill="#222222">open_rec_bvar</text>
 </a>
 </g>
 </g>
 <!-- open_rec_bvar&#45;&gt;open_rec_fvs -->
 <g id="edge3" class="edge">
 <title>open_rec_bvar&#45;&gt;open_rec_fvs</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M102.23,-521.95C111.91,-525.83 122.04,-530.81 130.48,-537 154.67,-554.72 149.23,-571.35 173.48,-589 181.18,-594.6 190.25,-599.2 199.15,-602.89"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="198.6,-604.94 204.95,-605.19 200.14,-601.03 198.6,-604.94"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M102.43,-530.9C130.77,-539.44 170.14,-551.29 199.31,-560.08"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="199.02,-562.19 205.37,-561.91 200.23,-558.17 199.02,-562.19"/>
 </g>
 <!-- open_close -->
 <g id="node11" class="node">
 <title>open_close</title>
 <g id="a_node11"><a xlink:title="open_close theory/Binding.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-511" rx="36.9" ry="18"/>
-<text text-anchor="middle" x="239.88" y="-508.8" font-family="Inter" font-size="9.00" fill="#222222">open_close</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-520" rx="36.9" ry="18"/>
+<text text-anchor="middle" x="239.88" y="-517.8" font-family="Inter" font-size="9.00" fill="#222222">open_close</text>
 </a>
 </g>
 </g>
 <!-- open_rec_bvar&#45;&gt;open_close -->
 <g id="edge5" class="edge">
 <title>open_rec_bvar&#45;&gt;open_close</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M111.6,-511C137.96,-511 170.95,-511 196.74,-511"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="196.79,-513.1 202.79,-511 196.79,-508.9 196.79,-513.1"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M111.6,-520C137.96,-520 170.95,-520 196.74,-520"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="196.79,-522.1 202.79,-520 196.79,-517.9 196.79,-522.1"/>
 </g>
 <!-- close_rec_fvar -->
 <g id="node5" class="node">
 <title>close_rec_fvar</title>
 <g id="a_node5"><a xlink:title="close_rec_fvar theory/Binding.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-771" rx="45.07" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-768.8" font-family="Inter" font-size="9.00" fill="#222222">close_rec_fvar</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-780" rx="45.07" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-777.8" font-family="Inter" font-size="9.00" fill="#222222">close_rec_fvar</text>
 </a>
 </g>
 </g>
@@ -138,8 +138,8 @@
 <g id="node6" class="node">
 <title>open_rec_occurs_false</title>
 <g id="a_node6"><a xlink:title="open_rec_occurs_false theory/Binding.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-196" rx="65.48" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-193.8" font-family="Inter" font-size="9.00" fill="#222222">open_rec_occurs_false</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-109" rx="65.48" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-106.8" font-family="Inter" font-size="9.00" fill="#222222">open_rec_occurs_false</text>
 </a>
 </g>
 </g>
@@ -147,47 +147,68 @@
 <g id="node22" class="node">
 <title>open_rec_zplug_lift</title>
 <g id="a_node22"><a xlink:title="open_rec_zplug_lift theory/Metatheory.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-122" rx="56.66" ry="18"/>
-<text text-anchor="middle" x="239.88" y="-119.8" font-family="Inter" font-size="9.00" fill="#222222">open_rec_zplug_lift</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-156" rx="56.66" ry="18"/>
+<text text-anchor="middle" x="239.88" y="-153.8" font-family="Inter" font-size="9.00" fill="#222222">open_rec_zplug_lift</text>
 </a>
 </g>
 </g>
 <!-- open_rec_occurs_false&#45;&gt;open_rec_zplug_lift -->
 <g id="edge13" class="edge">
 <title>open_rec_occurs_false&#45;&gt;open_rec_zplug_lift</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M99.89,-180.5C120.94,-170.91 148.68,-158.48 173.48,-148 181.1,-144.78 189.27,-141.44 197.16,-138.28"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="198.33,-140.07 203.13,-135.9 196.78,-136.17 198.33,-140.07"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M112.5,-121.6C136.54,-128.14 165.89,-136.13 190.25,-142.76"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="189.99,-144.87 196.34,-144.42 191.1,-140.82 189.99,-144.87"/>
 </g>
 <!-- full_comp_aux -->
 <g id="node23" class="node">
 <title>full_comp_aux</title>
 <g id="a_node23"><a xlink:title="full_comp_aux theory/Metatheory.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-139" rx="44.41" ry="18"/>
-<text text-anchor="middle" x="408.74" y="-136.8" font-family="Inter" font-size="9.00" fill="#222222">full_comp_aux</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-156" rx="44.41" ry="18"/>
+<text text-anchor="middle" x="408.74" y="-153.8" font-family="Inter" font-size="9.00" fill="#222222">full_comp_aux</text>
 </a>
 </g>
 </g>
 <!-- open_rec_occurs_false&#45;&gt;full_comp_aux -->
 <g id="edge16" class="edge">
 <title>open_rec_occurs_false&#45;&gt;full_comp_aux</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M120.34,-205.79C169.78,-212.67 244.39,-217.82 306.27,-200 327.96,-193.76 329.96,-184.67 349.27,-173 358.26,-167.57 368.1,-161.78 377.11,-156.55"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="378.16,-158.37 382.3,-153.54 376.06,-154.73 378.16,-158.37"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M129.77,-111.72C178.37,-114.49 246.89,-119.87 306.27,-130 326.24,-133.41 348.05,-138.77 366.31,-143.75"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="366.01,-145.85 372.36,-145.42 367.13,-141.8 366.01,-145.85"/>
+</g>
+<!-- subst_notin -->
+<g id="node68" class="node">
+<title>subst_notin</title>
+<g id="a_node68"><a xlink:title="subst_notin theory/Substitution.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-18" rx="37.56" ry="18"/>
+<text text-anchor="middle" x="239.88" y="-15.8" font-family="Inter" font-size="9.00" fill="#222222">subst_notin</text>
+</a>
+</g>
+</g>
+<!-- open_rec_occurs_false&#45;&gt;subst_notin -->
+<g id="edge53" class="edge">
+<title>open_rec_occurs_false&#45;&gt;subst_notin</title>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M91.13,-92.28C112.45,-78.36 144.24,-58.55 173.48,-44 182.99,-39.27 193.58,-34.75 203.43,-30.85"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="204.3,-32.77 209.12,-28.63 202.77,-28.85 204.3,-32.77"/>
 </g>
 <!-- close_rec_notin -->
 <g id="node7" class="node">
 <title>close_rec_notin</title>
 <g id="a_node7"><a xlink:title="close_rec_notin theory/Binding.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-823" rx="47.84" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-820.8" font-family="Inter" font-size="9.00" fill="#222222">close_rec_notin</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-18" rx="47.84" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-15.8" font-family="Inter" font-size="9.00" fill="#222222">close_rec_notin</text>
 </a>
 </g>
 </g>
+<!-- close_rec_notin&#45;&gt;subst_notin -->
+<g id="edge52" class="edge">
+<title>close_rec_notin&#45;&gt;subst_notin</title>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M113.41,-18C139.18,-18 170.86,-18 195.93,-18"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="196.16,-20.1 202.16,-18 196.16,-15.9 196.16,-20.1"/>
+</g>
 <!-- close_rec_fvs -->
 <g id="node8" class="node">
 <title>close_rec_fvs</title>
 <g id="a_node8"><a xlink:title="close_rec_fvs theory/Binding.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-667" rx="42.95" ry="18"/>
-<text text-anchor="middle" x="239.88" y="-664.8" font-family="Inter" font-size="9.00" fill="#222222">close_rec_fvs</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-624" rx="42.95" ry="18"/>
+<text text-anchor="middle" x="239.88" y="-621.8" font-family="Inter" font-size="9.00" fill="#222222">close_rec_fvs</text>
 </a>
 </g>
 </g>
@@ -195,53 +216,83 @@
 <g id="node14" class="node">
 <title>subst_fvs</title>
 <g id="a_node14"><a xlink:title="subst_fvs theory/Binding.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-667" rx="32.16" ry="18"/>
-<text text-anchor="middle" x="408.74" y="-664.8" font-family="Inter" font-size="9.00" fill="#222222">subst_fvs</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-572" rx="32.16" ry="18"/>
+<text text-anchor="middle" x="408.74" y="-569.8" font-family="Inter" font-size="9.00" fill="#222222">subst_fvs</text>
 </a>
 </g>
 </g>
 <!-- close_rec_fvs&#45;&gt;subst_fvs -->
 <g id="edge7" class="edge">
 <title>close_rec_fvs&#45;&gt;subst_fvs</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M282.98,-667C309.8,-667 344.23,-667 370.13,-667"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="370.18,-669.1 376.18,-667 370.18,-664.9 370.18,-669.1"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M274.64,-613.48C303.63,-604.44 345.18,-591.49 374.12,-582.48"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="374.99,-584.4 380.1,-580.61 373.74,-580.39 374.99,-584.4"/>
 </g>
 <!-- open_rec_bvar_neq -->
 <g id="node9" class="node">
 <title>open_rec_bvar_neq</title>
 <g id="a_node9"><a xlink:title="open_rec_bvar_neq theory/Binding.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-615" rx="57.97" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-612.8" font-family="Inter" font-size="9.00" fill="#222222">open_rec_bvar_neq</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-572" rx="57.97" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-569.8" font-family="Inter" font-size="9.00" fill="#222222">open_rec_bvar_neq</text>
 </a>
 </g>
 </g>
 <!-- open_rec_bvar_neq&#45;&gt;open_rec_fvs -->
 <g id="edge4" class="edge">
 <title>open_rec_bvar_neq&#45;&gt;open_rec_fvs</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M123.25,-615C145.5,-615 170.71,-615 191.9,-615"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="192.05,-617.1 198.05,-615 192.05,-612.9 192.05,-617.1"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M123.25,-572C145.5,-572 170.71,-572 191.9,-572"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="192.05,-574.1 198.05,-572 192.05,-569.9 192.05,-574.1"/>
 </g>
 <!-- open_rec_fvs&#45;&gt;subst_fvs -->
 <g id="edge8" class="edge">
 <title>open_rec_fvs&#45;&gt;subst_fvs</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M274.24,-625.4C303.28,-634.45 345.15,-647.49 374.23,-656.56"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="373.87,-658.65 380.23,-658.43 375.12,-654.64 373.87,-658.65"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M281.7,-572C308.67,-572 343.77,-572 370.08,-572"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="370.23,-574.1 376.23,-572 370.23,-569.9 370.23,-574.1"/>
+</g>
+<!-- subst_lc_self -->
+<g id="node69" class="node">
+<title>subst_lc_self</title>
+<g id="a_node69"><a xlink:title="subst_lc_self theory/Substitution.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="565.21" cy="-728" rx="40.33" ry="18"/>
+<text text-anchor="middle" x="565.21" y="-725.8" font-family="Inter" font-size="9.00" fill="#222222">subst_lc_self</text>
+</a>
+</g>
+</g>
+<!-- subst_fvar_self&#45;&gt;subst_lc_self -->
+<g id="edge54" class="edge">
+<title>subst_fvar_self&#45;&gt;subst_lc_self</title>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M454.42,-728C474.52,-728 498.23,-728 518.46,-728"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="518.62,-730.1 524.62,-728 518.62,-725.9 518.62,-730.1"/>
 </g>
 <!-- subst_fvar_other -->
 <g id="node13" class="node">
 <title>subst_fvar_other</title>
 <g id="a_node13"><a xlink:title="subst_fvar_other theory/Binding.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-875" rx="49.8" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-872.8" font-family="Inter" font-size="9.00" fill="#222222">subst_fvar_other</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-832" rx="49.8" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-829.8" font-family="Inter" font-size="9.00" fill="#222222">subst_fvar_other</text>
 </a>
 </g>
 </g>
+<!-- subst_other -->
+<g id="node70" class="node">
+<title>subst_other</title>
+<g id="a_node70"><a xlink:title="subst_other theory/Substitution.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-832" rx="37.56" ry="18"/>
+<text text-anchor="middle" x="239.88" y="-829.8" font-family="Inter" font-size="9.00" fill="#222222">subst_other</text>
+</a>
+</g>
+</g>
+<!-- subst_fvar_other&#45;&gt;subst_other -->
+<g id="edge55" class="edge">
+<title>subst_fvar_other&#45;&gt;subst_other</title>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M115.25,-832C140.7,-832 171.52,-832 196.02,-832"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="196.1,-834.1 202.1,-832 196.1,-829.9 196.1,-834.1"/>
+</g>
 <!-- Plus_red1_context -->
 <g id="node15" class="node">
 <title>Plus_red1_context</title>
 <g id="a_node15"><a xlink:title="Plus_red1_context theory/Metatheory.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="565.21" cy="-191" rx="53.23" ry="18"/>
-<text text-anchor="middle" x="565.21" y="-188.8" font-family="Inter" font-size="9.00" fill="#222222">Plus_red1_context</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="565.21" cy="-208" rx="53.23" ry="18"/>
+<text text-anchor="middle" x="565.21" y="-205.8" font-family="Inter" font-size="9.00" fill="#222222">Plus_red1_context</text>
 </a>
 </g>
 </g>
@@ -249,23 +300,23 @@
 <g id="node30" class="node">
 <title>lemma_2_3_beta_sim</title>
 <g id="a_node30"><a xlink:title="lemma_2_3_beta_sim (section 2.3) theory/Metatheory.v https://arxiv.org/html/2312.13270v1">
-<path fill="#d9ead3" stroke="#38761d" d="M763.21,-183C763.21,-183 681.21,-183 681.21,-183 675.21,-183 669.21,-177 669.21,-171 669.21,-171 669.21,-159 669.21,-159 669.21,-153 675.21,-147 681.21,-147 681.21,-147 763.21,-147 763.21,-147 769.21,-147 775.21,-153 775.21,-159 775.21,-159 775.21,-171 775.21,-171 775.21,-177 769.21,-183 763.21,-183"/>
-<text text-anchor="middle" x="722.21" y="-162.8" font-family="Inter" font-size="9.00" fill="#222222">lemma_2_3_beta_sim</text>
+<path fill="#d9ead3" stroke="#38761d" d="M763.21,-200C763.21,-200 681.21,-200 681.21,-200 675.21,-200 669.21,-194 669.21,-188 669.21,-188 669.21,-176 669.21,-176 669.21,-170 675.21,-164 681.21,-164 681.21,-164 763.21,-164 763.21,-164 769.21,-164 775.21,-170 775.21,-176 775.21,-176 775.21,-188 775.21,-188 775.21,-194 769.21,-200 763.21,-200"/>
+<text text-anchor="middle" x="722.21" y="-179.8" font-family="Inter" font-size="9.00" fill="#222222">lemma_2_3_beta_sim</text>
 </a>
 </g>
 </g>
 <!-- Plus_red1_context&#45;&gt;lemma_2_3_beta_sim -->
 <g id="edge26" class="edge">
 <title>Plus_red1_context&#45;&gt;lemma_2_3_beta_sim</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M613.13,-183.13C628.84,-180.49 646.55,-177.52 663.02,-174.76"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="663.46,-176.82 669.03,-173.75 662.76,-172.67 663.46,-176.82"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M613.13,-200.13C628.84,-197.49 646.55,-194.52 663.02,-191.76"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="663.46,-193.82 669.03,-190.75 662.76,-189.67 663.46,-193.82"/>
 </g>
 <!-- occurs_count_zero -->
 <g id="node16" class="node">
 <title>occurs_count_zero</title>
 <g id="a_node16"><a xlink:title="occurs_count_zero theory/Metatheory.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-18" rx="54.7" ry="18"/>
-<text text-anchor="middle" x="239.88" y="-15.8" font-family="Inter" font-size="9.00" fill="#222222">occurs_count_zero</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-70" rx="54.7" ry="18"/>
+<text text-anchor="middle" x="239.88" y="-67.8" font-family="Inter" font-size="9.00" fill="#222222">occurs_count_zero</text>
 </a>
 </g>
 </g>
@@ -273,29 +324,29 @@
 <g id="node18" class="node">
 <title>occurs_count_pos</title>
 <g id="a_node18"><a xlink:title="occurs_count_pos theory/Metatheory.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-18" rx="53.89" ry="18"/>
-<text text-anchor="middle" x="408.74" y="-15.8" font-family="Inter" font-size="9.00" fill="#222222">occurs_count_pos</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-70" rx="53.89" ry="18"/>
+<text text-anchor="middle" x="408.74" y="-67.8" font-family="Inter" font-size="9.00" fill="#222222">occurs_count_pos</text>
 </a>
 </g>
 </g>
 <!-- occurs_count_zero&#45;&gt;occurs_count_pos -->
 <g id="edge9" class="edge">
 <title>occurs_count_zero&#45;&gt;occurs_count_pos</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M295.05,-18C312.17,-18 331.17,-18 348.62,-18"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="348.97,-20.1 354.97,-18 348.97,-15.9 348.97,-20.1"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M295.05,-70C312.17,-70 331.17,-70 348.62,-70"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="348.97,-72.1 354.97,-70 348.97,-67.9 348.97,-72.1"/>
 </g>
 <!-- occurs_count_zero&#45;&gt;full_comp_aux -->
 <g id="edge14" class="edge">
 <title>occurs_count_zero&#45;&gt;full_comp_aux</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M279.4,-30.54C288.54,-34.26 298.02,-38.76 306.27,-44 338.66,-64.56 369.95,-96.22 389.02,-117.26"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="387.56,-118.78 393.13,-121.85 390.69,-115.98 387.56,-118.78"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M273.37,-84.33C283.94,-89.15 295.68,-94.66 306.27,-100 330.41,-112.18 357.16,-127 377.13,-138.33"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="376.33,-140.29 382.58,-141.43 378.41,-136.64 376.33,-140.29"/>
 </g>
 <!-- occurs_count_false -->
 <g id="node17" class="node">
 <title>occurs_count_false</title>
 <g id="a_node17"><a xlink:title="occurs_count_false theory/Metatheory.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-70" rx="56.66" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-67.8" font-family="Inter" font-size="9.00" fill="#222222">occurs_count_false</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-213" rx="56.66" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-210.8" font-family="Inter" font-size="9.00" fill="#222222">occurs_count_false</text>
 </a>
 </g>
 </g>
@@ -303,107 +354,107 @@
 <g id="node21" class="node">
 <title>occurs_count_zfill_plug</title>
 <g id="a_node21"><a xlink:title="occurs_count_zfill_plug theory/Metatheory.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-70" rx="66.29" ry="18"/>
-<text text-anchor="middle" x="239.88" y="-67.8" font-family="Inter" font-size="9.00" fill="#222222">occurs_count_zfill_plug</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-208" rx="66.29" ry="18"/>
+<text text-anchor="middle" x="239.88" y="-205.8" font-family="Inter" font-size="9.00" fill="#222222">occurs_count_zfill_plug</text>
 </a>
 </g>
 </g>
 <!-- occurs_count_false&#45;&gt;occurs_count_zfill_plug -->
 <g id="edge10" class="edge">
 <title>occurs_count_false&#45;&gt;occurs_count_zfill_plug</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M122.29,-70C136.5,-70 151.97,-70 166.86,-70"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="167.2,-72.1 173.2,-70 167.2,-67.9 167.2,-72.1"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M121.81,-211.39C136.43,-210.97 152.41,-210.5 167.72,-210.06"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="167.84,-212.16 173.78,-209.89 167.72,-207.96 167.84,-212.16"/>
 </g>
 <!-- occurs_lift_self -->
 <g id="node19" class="node">
 <title>occurs_lift_self</title>
 <g id="a_node19"><a xlink:title="occurs_lift_self theory/Metatheory.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-122" rx="46.38" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-119.8" font-family="Inter" font-size="9.00" fill="#222222">occurs_lift_self</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-161" rx="46.38" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-158.8" font-family="Inter" font-size="9.00" fill="#222222">occurs_lift_self</text>
 </a>
 </g>
 </g>
 <!-- occurs_lift_self&#45;&gt;occurs_count_zfill_plug -->
 <g id="edge11" class="edge">
 <title>occurs_lift_self&#45;&gt;occurs_count_zfill_plug</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M102.43,-111.1C127.54,-103.54 161.3,-93.37 188.96,-85.03"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="189.63,-87.03 194.77,-83.29 188.42,-83.01 189.63,-87.03"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M103.7,-171.2C127.85,-177.77 159.62,-186.42 186.29,-193.68"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="185.91,-195.76 192.25,-195.31 187.01,-191.7 185.91,-195.76"/>
 </g>
 <!-- occurs_lift_self&#45;&gt;open_rec_zplug_lift -->
 <g id="edge12" class="edge">
 <title>occurs_lift_self&#45;&gt;open_rec_zplug_lift</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M111.6,-122C131.6,-122 155.41,-122 177.01,-122"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="177.03,-124.1 183.03,-122 177.03,-119.9 177.03,-124.1"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M111.6,-159.69C131.69,-159.1 155.63,-158.41 177.3,-157.78"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="177.41,-159.88 183.35,-157.61 177.29,-155.68 177.41,-159.88"/>
 </g>
 <!-- zdecs_nonempty -->
 <g id="node20" class="node">
 <title>zdecs_nonempty</title>
 <g id="a_node20"><a xlink:title="zdecs_nonempty theory/Metatheory.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-174" rx="51.27" ry="18"/>
-<text text-anchor="middle" x="239.88" y="-171.8" font-family="Inter" font-size="9.00" fill="#222222">zdecs_nonempty</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-260" rx="51.27" ry="18"/>
+<text text-anchor="middle" x="239.88" y="-257.8" font-family="Inter" font-size="9.00" fill="#222222">zdecs_nonempty</text>
 </a>
 </g>
 </g>
 <!-- zdecs_nonempty&#45;&gt;full_comp_aux -->
 <g id="edge18" class="edge">
 <title>zdecs_nonempty&#45;&gt;full_comp_aux</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M284.28,-164.9C308.41,-159.84 338.38,-153.55 362.75,-148.44"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="363.38,-150.45 368.82,-147.16 362.52,-146.34 363.38,-150.45"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M279.56,-248.33C288.79,-244.56 298.27,-239.82 306.27,-234 330.52,-216.35 325.38,-200.13 349.27,-182 355.15,-177.54 361.91,-173.65 368.7,-170.32"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="369.85,-172.1 374.4,-167.66 368.07,-168.3 369.85,-172.1"/>
 </g>
 <!-- occurs_count_zfill_plug&#45;&gt;full_comp_aux -->
 <g id="edge15" class="edge">
 <title>occurs_count_zfill_plug&#45;&gt;full_comp_aux</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M278.28,-84.71C287.45,-88.36 297.23,-92.29 306.27,-96 328.08,-104.96 352.41,-115.26 371.78,-123.53"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="371.28,-125.6 377.62,-126.03 372.93,-121.74 371.28,-125.6"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M284.28,-194.47C309.85,-186.51 341.99,-176.49 367.07,-168.67"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="367.85,-170.63 372.95,-166.84 366.6,-166.62 367.85,-170.63"/>
 </g>
 <!-- open_rec_zplug_lift&#45;&gt;full_comp_aux -->
 <g id="edge17" class="edge">
 <title>open_rec_zplug_lift&#45;&gt;full_comp_aux</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M294.13,-127.43C315.05,-129.56 338.89,-131.99 359.31,-134.07"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="359.35,-136.18 365.54,-134.7 359.78,-132 359.35,-136.18"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M296.9,-156C316.72,-156 338.87,-156 358.12,-156"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="358.26,-158.1 364.26,-156 358.26,-153.9 358.26,-158.1"/>
 </g>
 <!-- lemma_2_2_full_comp -->
 <g id="node24" class="node">
 <title>lemma_2_2_full_comp</title>
 <g id="a_node24"><a xlink:title="lemma_2_2_full_comp (section 2.2) theory/Metatheory.v https://arxiv.org/html/2312.13270v1">
-<path fill="#d9ead3" stroke="#38761d" d="M607.21,-157C607.21,-157 523.21,-157 523.21,-157 517.21,-157 511.21,-151 511.21,-145 511.21,-145 511.21,-133 511.21,-133 511.21,-127 517.21,-121 523.21,-121 523.21,-121 607.21,-121 607.21,-121 613.21,-121 619.21,-127 619.21,-133 619.21,-133 619.21,-145 619.21,-145 619.21,-151 613.21,-157 607.21,-157"/>
-<text text-anchor="middle" x="565.21" y="-136.8" font-family="Inter" font-size="9.00" fill="#222222">lemma_2_2_full_comp</text>
+<path fill="#d9ead3" stroke="#38761d" d="M607.21,-174C607.21,-174 523.21,-174 523.21,-174 517.21,-174 511.21,-168 511.21,-162 511.21,-162 511.21,-150 511.21,-150 511.21,-144 517.21,-138 523.21,-138 523.21,-138 607.21,-138 607.21,-138 613.21,-138 619.21,-144 619.21,-150 619.21,-150 619.21,-162 619.21,-162 619.21,-168 613.21,-174 607.21,-174"/>
+<text text-anchor="middle" x="565.21" y="-153.8" font-family="Inter" font-size="9.00" fill="#222222">lemma_2_2_full_comp</text>
 </a>
 </g>
 </g>
 <!-- full_comp_aux&#45;&gt;lemma_2_2_full_comp -->
 <g id="edge20" class="edge">
 <title>full_comp_aux&#45;&gt;lemma_2_2_full_comp</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M453.59,-139C469.56,-139 487.88,-139 504.96,-139"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="505.19,-141.1 511.19,-139 505.19,-136.9 505.19,-141.1"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M453.59,-156C469.56,-156 487.88,-156 504.96,-156"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="505.19,-158.1 511.19,-156 505.19,-153.9 505.19,-158.1"/>
 </g>
 <!-- lemma_2_2_full_comp&#45;&gt;lemma_2_3_beta_sim -->
 <g id="edge27" class="edge">
 <title>lemma_2_2_full_comp&#45;&gt;lemma_2_3_beta_sim</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M619.55,-147.95C633.57,-150.3 648.76,-152.85 663.03,-155.24"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="662.81,-157.33 669.08,-156.26 663.51,-153.19 662.81,-157.33"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M619.55,-164.95C633.57,-167.3 648.76,-169.85 663.03,-172.24"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="662.81,-174.33 669.08,-173.26 663.51,-170.19 662.81,-174.33"/>
 </g>
 <!-- red1_root_fv -->
 <g id="node27" class="node">
 <title>red1_root_fv</title>
 <g id="a_node27"><a xlink:title="red1_root_fv theory/Metatheory.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-563" rx="38.87" ry="18"/>
-<text text-anchor="middle" x="408.74" y="-560.8" font-family="Inter" font-size="9.00" fill="#222222">red1_root_fv</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-676" rx="38.87" ry="18"/>
+<text text-anchor="middle" x="408.74" y="-673.8" font-family="Inter" font-size="9.00" fill="#222222">red1_root_fv</text>
 </a>
 </g>
 </g>
 <!-- fvs_zplug_lift&#45;&gt;red1_root_fv -->
 <g id="edge22" class="edge">
 <title>fvs_zplug_lift&#45;&gt;red1_root_fv</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M281.27,-563C306.27,-563 338.37,-563 363.98,-563"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="364.01,-565.1 370.01,-563 364.01,-560.9 364.01,-565.1"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M281.27,-676C306.27,-676 338.37,-676 363.98,-676"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="364.01,-678.1 370.01,-676 364.01,-673.9 364.01,-678.1"/>
 </g>
 <!-- plug_fv_mono -->
 <g id="node26" class="node">
 <title>plug_fv_mono</title>
 <g id="a_node26"><a xlink:title="plug_fv_mono theory/Metatheory.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-615" rx="42.95" ry="18"/>
-<text text-anchor="middle" x="408.74" y="-612.8" font-family="Inter" font-size="9.00" fill="#222222">plug_fv_mono</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-624" rx="42.95" ry="18"/>
+<text text-anchor="middle" x="408.74" y="-621.8" font-family="Inter" font-size="9.00" fill="#222222">plug_fv_mono</text>
 </a>
 </g>
 </g>
@@ -411,343 +462,676 @@
 <g id="node28" class="node">
 <title>red1r_fv</title>
 <g id="a_node28"><a xlink:title="red1r_fv theory/Metatheory.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="565.21" cy="-563" rx="28.74" ry="18"/>
-<text text-anchor="middle" x="565.21" y="-560.8" font-family="Inter" font-size="9.00" fill="#222222">red1r_fv</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="565.21" cy="-624" rx="28.74" ry="18"/>
+<text text-anchor="middle" x="565.21" y="-621.8" font-family="Inter" font-size="9.00" fill="#222222">red1r_fv</text>
 </a>
 </g>
 </g>
 <!-- plug_fv_mono&#45;&gt;red1r_fv -->
 <g id="edge23" class="edge">
 <title>plug_fv_mono&#45;&gt;red1r_fv</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M442.88,-603.84C469.74,-594.8 507.32,-582.15 533.51,-573.33"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="534.23,-575.31 539.24,-571.4 532.89,-571.33 534.23,-575.31"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M451.54,-624C476.15,-624 506.88,-624 530.03,-624"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="530.04,-626.1 536.04,-624 530.04,-621.9 530.04,-626.1"/>
 </g>
 <!-- red1_root_fv&#45;&gt;red1r_fv -->
 <g id="edge24" class="edge">
 <title>red1_root_fv&#45;&gt;red1r_fv</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M447.53,-563C472.72,-563 505.57,-563 530,-563"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="530.01,-565.1 536.01,-563 530.01,-560.9 530.01,-565.1"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M440.63,-665.6C467.64,-656.51 506.65,-643.38 533.58,-634.31"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="534.46,-636.23 539.48,-632.33 533.12,-632.25 534.46,-636.23"/>
 </g>
 <!-- lemma_2_1_fv_preserved -->
 <g id="node29" class="node">
 <title>lemma_2_1_fv_preserved</title>
 <g id="a_node29"><a xlink:title="lemma_2_1_fv_preserved (section 2.1) theory/Metatheory.v https://arxiv.org/html/2312.13270v1">
-<path fill="#d9ead3" stroke="#38761d" d="M770.21,-555C770.21,-555 674.21,-555 674.21,-555 668.21,-555 662.21,-549 662.21,-543 662.21,-543 662.21,-531 662.21,-531 662.21,-525 668.21,-519 674.21,-519 674.21,-519 770.21,-519 770.21,-519 776.21,-519 782.21,-525 782.21,-531 782.21,-531 782.21,-543 782.21,-543 782.21,-549 776.21,-555 770.21,-555"/>
-<text text-anchor="middle" x="722.21" y="-534.8" font-family="Inter" font-size="9.00" fill="#222222">lemma_2_1_fv_preserved</text>
+<path fill="#d9ead3" stroke="#38761d" d="M770.21,-629C770.21,-629 674.21,-629 674.21,-629 668.21,-629 662.21,-623 662.21,-617 662.21,-617 662.21,-605 662.21,-605 662.21,-599 668.21,-593 674.21,-593 674.21,-593 770.21,-593 770.21,-593 776.21,-593 782.21,-599 782.21,-605 782.21,-605 782.21,-617 782.21,-617 782.21,-623 776.21,-629 770.21,-629"/>
+<text text-anchor="middle" x="722.21" y="-608.8" font-family="Inter" font-size="9.00" fill="#222222">lemma_2_1_fv_preserved</text>
 </a>
 </g>
 </g>
 <!-- red1r_fv&#45;&gt;lemma_2_1_fv_preserved -->
 <g id="edge25" class="edge">
 <title>red1r_fv&#45;&gt;lemma_2_1_fv_preserved</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M593.2,-558.47C610.57,-555.56 633.92,-551.64 655.92,-547.95"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="656.52,-549.98 662.09,-546.92 655.82,-545.84 656.52,-549.98"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M593.92,-621.68C611.19,-620.23 634.18,-618.3 655.87,-616.48"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="656.15,-618.56 661.95,-615.97 655.79,-614.38 656.15,-618.56"/>
+</g>
+<!-- gen_fv_preserved -->
+<g id="node42" class="node">
+<title>gen_fv_preserved</title>
+<g id="a_node42"><a xlink:title="gen_fv_preserved theory/Random.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="885.25" cy="-559" rx="52.58" ry="18"/>
+<text text-anchor="middle" x="885.25" y="-556.8" font-family="Inter" font-size="9.00" fill="#222222">gen_fv_preserved</text>
+</a>
+</g>
+</g>
+<!-- lemma_2_1_fv_preserved&#45;&gt;gen_fv_preserved -->
+<g id="edge35" class="edge">
+<title>lemma_2_1_fv_preserved&#45;&gt;gen_fv_preserved</title>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M779.08,-592.96C799.17,-586.47 821.52,-579.25 840.44,-573.15"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="841.13,-575.13 846.19,-571.29 839.84,-571.13 841.13,-575.13"/>
 </g>
 <!-- corpus_fv_preserved -->
-<g id="node50" class="node">
+<g id="node82" class="node">
 <title>corpus_fv_preserved</title>
-<g id="a_node50"><a xlink:title="corpus_fv_preserved theory/Tests.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="885.25" cy="-481" rx="60.09" ry="18"/>
-<text text-anchor="middle" x="885.25" y="-478.8" font-family="Inter" font-size="9.00" fill="#222222">corpus_fv_preserved</text>
+<g id="a_node82"><a xlink:title="corpus_fv_preserved theory/Tests.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="885.25" cy="-611" rx="60.09" ry="18"/>
+<text text-anchor="middle" x="885.25" y="-608.8" font-family="Inter" font-size="9.00" fill="#222222">corpus_fv_preserved</text>
 </a>
 </g>
 </g>
 <!-- lemma_2_1_fv_preserved&#45;&gt;corpus_fv_preserved -->
-<g id="edge46" class="edge">
+<g id="edge62" class="edge">
 <title>lemma_2_1_fv_preserved&#45;&gt;corpus_fv_preserved</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M775.05,-518.97C795.8,-511.76 819.48,-503.52 839.47,-496.57"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="840.3,-498.51 845.28,-494.55 838.92,-494.54 840.3,-498.51"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M782.26,-611C794.18,-611 806.79,-611 818.91,-611"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="819.2,-613.1 825.2,-611 819.2,-608.9 819.2,-613.1"/>
+</g>
+<!-- par_red1_iff -->
+<g id="node31" class="node">
+<title>par_red1_iff</title>
+<g id="a_node31"><a xlink:title="par_red1_iff theory/Parallel.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-884" rx="37.56" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-881.8" font-family="Inter" font-size="9.00" fill="#222222">par_red1_iff</text>
+</a>
+</g>
+</g>
+<!-- par_to_red1_or_eq -->
+<g id="node34" class="node">
+<title>par_to_red1_or_eq</title>
+<g id="a_node34"><a xlink:title="par_to_red1_or_eq theory/Parallel.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-936" rx="53.23" ry="18"/>
+<text text-anchor="middle" x="239.88" y="-933.8" font-family="Inter" font-size="9.00" fill="#222222">par_to_red1_or_eq</text>
+</a>
+</g>
+</g>
+<!-- par_red1_iff&#45;&gt;par_to_red1_or_eq -->
+<g id="edge28" class="edge">
+<title>par_red1_iff&#45;&gt;par_to_red1_or_eq</title>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M97.5,-893.42C124.38,-901.51 163.47,-913.29 193.73,-922.4"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="193.31,-924.47 199.66,-924.19 194.53,-920.45 193.31,-924.47"/>
+</g>
+<!-- red1_or_eq_to_par -->
+<g id="node35" class="node">
+<title>red1_or_eq_to_par</title>
+<g id="a_node35"><a xlink:title="red1_or_eq_to_par theory/Parallel.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-884" rx="53.23" ry="18"/>
+<text text-anchor="middle" x="239.88" y="-881.8" font-family="Inter" font-size="9.00" fill="#222222">red1_or_eq_to_par</text>
+</a>
+</g>
+</g>
+<!-- par_red1_iff&#45;&gt;red1_or_eq_to_par -->
+<g id="edge29" class="edge">
+<title>par_red1_iff&#45;&gt;red1_or_eq_to_par</title>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M102.85,-884C125.39,-884 154.79,-884 180.49,-884"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="180.6,-886.1 186.6,-884 180.6,-881.9 180.6,-886.1"/>
+</g>
+<!-- red1_in_par -->
+<g id="node32" class="node">
+<title>red1_in_par</title>
+<g id="a_node32"><a xlink:title="red1_in_par theory/Parallel.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-936" rx="37.56" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-933.8" font-family="Inter" font-size="9.00" fill="#222222">red1_in_par</text>
+</a>
+</g>
+</g>
+<!-- par_context -->
+<g id="node33" class="node">
+<title>par_context</title>
+<g id="a_node33"><a xlink:title="par_context theory/Parallel.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-988" rx="38.87" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-985.8" font-family="Inter" font-size="9.00" fill="#222222">par_context</text>
+</a>
+</g>
+</g>
+<!-- par_reflexive -->
+<g id="node36" class="node">
+<title>par_reflexive</title>
+<g id="a_node36"><a xlink:title="par_reflexive theory/Parallel.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1040" rx="41.64" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-1037.8" font-family="Inter" font-size="9.00" fill="#222222">par_reflexive</text>
+</a>
+</g>
+</g>
+<!-- gen_list_length -->
+<g id="node37" class="node">
+<title>gen_list_length</title>
+<g id="a_node37"><a xlink:title="gen_list_length theory/Random.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1092" rx="46.38" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-1089.8" font-family="Inter" font-size="9.00" fill="#222222">gen_list_length</text>
+</a>
+</g>
+</g>
+<!-- check_term_true -->
+<g id="node38" class="node">
+<title>check_term_true</title>
+<g id="a_node38"><a xlink:title="check_term_true theory/Random.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="885.25" cy="-494" rx="50.61" ry="18"/>
+<text text-anchor="middle" x="885.25" y="-491.8" font-family="Inter" font-size="9.00" fill="#222222">check_term_true</text>
+</a>
+</g>
+</g>
+<!-- check_all_true -->
+<g id="node39" class="node">
+<title>check_all_true</title>
+<g id="a_node39"><a xlink:title="check_all_true theory/Random.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="1032.75" cy="-494" rx="44.41" ry="18"/>
+<text text-anchor="middle" x="1032.75" y="-491.8" font-family="Inter" font-size="9.00" fill="#222222">check_all_true</text>
+</a>
+</g>
+</g>
+<!-- check_term_true&#45;&gt;check_all_true -->
+<g id="edge32" class="edge">
+<title>check_term_true&#45;&gt;check_all_true</title>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M936.32,-494C951,-494 967.04,-494 981.71,-494"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="981.9,-496.1 987.9,-494 981.9,-491.9 981.9,-496.1"/>
+</g>
+<!-- gen_sound -->
+<g id="node40" class="node">
+<title>gen_sound</title>
+<g id="a_node40"><a xlink:title="gen_sound theory/Random.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="722.21" cy="-507" rx="35.59" ry="18"/>
+<text text-anchor="middle" x="722.21" y="-504.8" font-family="Inter" font-size="9.00" fill="#222222">gen_sound</text>
+</a>
+</g>
+</g>
+<!-- gen_complete -->
+<g id="node41" class="node">
+<title>gen_complete</title>
+<g id="a_node41"><a xlink:title="gen_complete theory/Random.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="722.21" cy="-325" rx="43.76" ry="18"/>
+<text text-anchor="middle" x="722.21" y="-322.8" font-family="Inter" font-size="9.00" fill="#222222">gen_complete</text>
+</a>
+</g>
 </g>
 <!-- zdecs_sound -->
-<g id="node31" class="node">
+<g id="node43" class="node">
 <title>zdecs_sound</title>
-<g id="a_node31"><a xlink:title="zdecs_sound theory/Reduction.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-260" rx="40.98" ry="18"/>
-<text text-anchor="middle" x="239.88" y="-257.8" font-family="Inter" font-size="9.00" fill="#222222">zdecs_sound</text>
+<g id="a_node43"><a xlink:title="zdecs_sound theory/Reduction.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-338" rx="40.98" ry="18"/>
+<text text-anchor="middle" x="239.88" y="-335.8" font-family="Inter" font-size="9.00" fill="#222222">zdecs_sound</text>
 </a>
 </g>
 </g>
 <!-- zdecs_sound&#45;&gt;full_comp_aux -->
 <g id="edge19" class="edge">
 <title>zdecs_sound&#45;&gt;full_comp_aux</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M272.62,-249.16C283.94,-244.37 296.34,-237.98 306.27,-230 331,-210.11 325.53,-194.06 349.27,-173 356.62,-166.48 365.41,-160.59 373.91,-155.62"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="374.97,-157.43 379.15,-152.64 372.9,-153.78 374.97,-157.43"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M264.56,-323.56C278.24,-314.24 294.93,-301.06 306.27,-286 336.36,-246.05 314.37,-217.83 349.27,-182 354.3,-176.84 360.53,-172.63 367.03,-169.21"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="368.07,-171.04 372.54,-166.52 366.22,-167.27 368.07,-171.04"/>
 </g>
 <!-- root_steps_sound -->
-<g id="node34" class="node">
+<g id="node46" class="node">
 <title>root_steps_sound</title>
-<g id="a_node34"><a xlink:title="root_steps_sound theory/Reduction.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-407" rx="51.27" ry="18"/>
-<text text-anchor="middle" x="408.74" y="-404.8" font-family="Inter" font-size="9.00" fill="#222222">root_steps_sound</text>
+<g id="a_node46"><a xlink:title="root_steps_sound theory/Reduction.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-364" rx="51.27" ry="18"/>
+<text text-anchor="middle" x="408.74" y="-361.8" font-family="Inter" font-size="9.00" fill="#222222">root_steps_sound</text>
 </a>
 </g>
 </g>
 <!-- zdecs_sound&#45;&gt;root_steps_sound -->
-<g id="edge28" class="edge">
+<g id="edge37" class="edge">
 <title>zdecs_sound&#45;&gt;root_steps_sound</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M276.31,-268.53C286.94,-272.46 297.96,-278.07 306.27,-286 339.8,-318 316.39,-348.34 349.27,-381 353.65,-385.35 358.87,-389.03 364.37,-392.13"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="363.66,-394.13 369.95,-395.05 365.6,-390.41 363.66,-394.13"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M278.74,-343.9C301.34,-347.42 330.39,-351.95 355.19,-355.81"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="355.14,-357.93 361.4,-356.78 355.79,-353.78 355.14,-357.93"/>
 </g>
 <!-- zdecs_complete -->
-<g id="node32" class="node">
+<g id="node44" class="node">
 <title>zdecs_complete</title>
-<g id="a_node32"><a xlink:title="zdecs_complete theory/Reduction.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-459" rx="49.15" ry="18"/>
-<text text-anchor="middle" x="239.88" y="-456.8" font-family="Inter" font-size="9.00" fill="#222222">zdecs_complete</text>
+<g id="a_node44"><a xlink:title="zdecs_complete theory/Reduction.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-416" rx="49.15" ry="18"/>
+<text text-anchor="middle" x="239.88" y="-413.8" font-family="Inter" font-size="9.00" fill="#222222">zdecs_complete</text>
 </a>
 </g>
 </g>
 <!-- root_steps_complete -->
-<g id="node35" class="node">
+<g id="node47" class="node">
 <title>root_steps_complete</title>
-<g id="a_node35"><a xlink:title="root_steps_complete theory/Reduction.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-459" rx="59.43" ry="18"/>
-<text text-anchor="middle" x="408.74" y="-456.8" font-family="Inter" font-size="9.00" fill="#222222">root_steps_complete</text>
+<g id="a_node47"><a xlink:title="root_steps_complete theory/Reduction.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-416" rx="59.43" ry="18"/>
+<text text-anchor="middle" x="408.74" y="-413.8" font-family="Inter" font-size="9.00" fill="#222222">root_steps_complete</text>
 </a>
 </g>
 </g>
 <!-- zdecs_complete&#45;&gt;root_steps_complete -->
-<g id="edge29" class="edge">
+<g id="edge38" class="edge">
 <title>zdecs_complete&#45;&gt;root_steps_complete</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M289.14,-459C306,-459 325.21,-459 343.19,-459"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="343.23,-461.1 349.23,-459 343.23,-456.9 343.23,-461.1"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M289.14,-416C306,-416 325.21,-416 343.19,-416"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="343.23,-418.1 349.23,-416 343.23,-413.9 343.23,-418.1"/>
 </g>
 <!-- positions_at -->
-<g id="node33" class="node">
+<g id="node45" class="node">
 <title>positions_at</title>
-<g id="a_node33"><a xlink:title="positions_at theory/Reduction.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-511" rx="38.21" ry="18"/>
-<text text-anchor="middle" x="408.74" y="-508.8" font-family="Inter" font-size="9.00" fill="#222222">positions_at</text>
+<g id="a_node45"><a xlink:title="positions_at theory/Reduction.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-520" rx="38.21" ry="18"/>
+<text text-anchor="middle" x="408.74" y="-517.8" font-family="Inter" font-size="9.00" fill="#222222">positions_at</text>
 </a>
 </g>
 </g>
 <!-- steps_sound -->
-<g id="node36" class="node">
+<g id="node48" class="node">
 <title>steps_sound</title>
-<g id="a_node36"><a xlink:title="steps_sound theory/Reduction.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="565.21" cy="-428" rx="39.02" ry="18"/>
-<text text-anchor="middle" x="565.21" y="-425.8" font-family="Inter" font-size="9.00" fill="#222222">steps_sound</text>
+<g id="a_node48"><a xlink:title="steps_sound theory/Reduction.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="565.21" cy="-481" rx="39.02" ry="18"/>
+<text text-anchor="middle" x="565.21" y="-478.8" font-family="Inter" font-size="9.00" fill="#222222">steps_sound</text>
 </a>
 </g>
 </g>
 <!-- positions_at&#45;&gt;steps_sound -->
-<g id="edge30" class="edge">
+<g id="edge39" class="edge">
 <title>positions_at&#45;&gt;steps_sound</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M438.01,-499.23C447.7,-494.98 458.53,-490 468.21,-485 491.66,-472.88 517.33,-457.52 536.22,-445.8"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="537.38,-447.55 541.36,-442.6 535.16,-443.99 537.38,-447.55"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M442.88,-511.63C466.76,-505.6 499.1,-497.44 524.39,-491.05"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="525.02,-493.06 530.32,-489.55 523.99,-488.99 525.02,-493.06"/>
 </g>
 <!-- root_steps_sound&#45;&gt;steps_sound -->
-<g id="edge31" class="edge">
+<g id="edge40" class="edge">
 <title>root_steps_sound&#45;&gt;steps_sound</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M456.92,-413.41C477.35,-416.19 501.09,-419.42 521.04,-422.13"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="520.87,-424.23 527.1,-422.96 521.44,-420.07 520.87,-424.23"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M444.47,-377.11C452.54,-380.79 460.91,-385.13 468.21,-390 476.48,-395.52 517.51,-435.23 543.18,-460.34"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="542.02,-462.15 547.78,-464.85 544.96,-459.15 542.02,-462.15"/>
 </g>
 <!-- steps_complete -->
-<g id="node43" class="node">
+<g id="node55" class="node">
 <title>steps_complete</title>
-<g id="a_node43"><a xlink:title="steps_complete theory/Reduction.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="565.21" cy="-316" rx="47.84" ry="18"/>
-<text text-anchor="middle" x="565.21" y="-313.8" font-family="Inter" font-size="9.00" fill="#222222">steps_complete</text>
+<g id="a_node55"><a xlink:title="steps_complete theory/Reduction.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="565.21" cy="-318" rx="47.84" ry="18"/>
+<text text-anchor="middle" x="565.21" y="-315.8" font-family="Inter" font-size="9.00" fill="#222222">steps_complete</text>
 </a>
 </g>
 </g>
 <!-- root_steps_complete&#45;&gt;steps_complete -->
-<g id="edge37" class="edge">
+<g id="edge46" class="edge">
 <title>root_steps_complete&#45;&gt;steps_complete</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M449.47,-445.8C456.24,-442.36 462.81,-438.13 468.21,-433 498.88,-403.82 482.41,-379.04 511.21,-348 516.35,-342.46 522.66,-337.55 529.12,-333.34"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="530.56,-334.92 534.55,-329.97 528.35,-331.35 530.56,-334.92"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M445.32,-401.71C453.03,-398.2 461.02,-394.22 468.21,-390 493.99,-374.86 521.03,-354.07 539.82,-338.72"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="541.6,-339.98 544.89,-334.54 538.93,-336.74 541.6,-339.98"/>
+</g>
+<!-- steps_sound&#45;&gt;gen_sound -->
+<g id="edge33" class="edge">
+<title>steps_sound&#45;&gt;gen_sound</title>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M602.55,-487.1C626.39,-491.09 657.54,-496.32 681.95,-500.42"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="681.74,-502.51 688,-501.43 682.43,-498.37 681.74,-502.51"/>
 </g>
 <!-- steps_sound_red1 -->
-<g id="node37" class="node">
+<g id="node49" class="node">
 <title>steps_sound_red1</title>
-<g id="a_node37"><a xlink:title="steps_sound_red1 theory/Reduction.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="722.21" cy="-480" rx="51.92" ry="18"/>
-<text text-anchor="middle" x="722.21" y="-477.8" font-family="Inter" font-size="9.00" fill="#222222">steps_sound_red1</text>
+<g id="a_node49"><a xlink:title="steps_sound_red1 theory/Reduction.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="722.21" cy="-559" rx="51.92" ry="18"/>
+<text text-anchor="middle" x="722.21" y="-556.8" font-family="Inter" font-size="9.00" fill="#222222">steps_sound_red1</text>
 </a>
 </g>
 </g>
 <!-- steps_sound&#45;&gt;steps_sound_red1 -->
-<g id="edge32" class="edge">
+<g id="edge41" class="edge">
 <title>steps_sound&#45;&gt;steps_sound_red1</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M597.57,-438.52C620.85,-446.33 652.85,-457.07 678.46,-465.66"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="677.8,-467.65 684.16,-467.57 679.14,-463.67 677.8,-467.65"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M590.78,-495.03C610.01,-505.83 637.53,-520.9 662.21,-533 668.8,-536.23 675.89,-539.52 682.79,-542.61"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="682.19,-544.64 688.53,-545.17 683.9,-540.81 682.19,-544.64"/>
 </g>
 <!-- has_red_spec -->
-<g id="node45" class="node">
+<g id="node57" class="node">
 <title>has_red_spec</title>
-<g id="a_node45"><a xlink:title="has_red_spec theory/Reduction.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="722.21" cy="-374" rx="42.95" ry="18"/>
-<text text-anchor="middle" x="722.21" y="-371.8" font-family="Inter" font-size="9.00" fill="#222222">has_red_spec</text>
+<g id="a_node57"><a xlink:title="has_red_spec theory/Reduction.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="722.21" cy="-403" rx="42.95" ry="18"/>
+<text text-anchor="middle" x="722.21" y="-400.8" font-family="Inter" font-size="9.00" fill="#222222">has_red_spec</text>
 </a>
 </g>
 </g>
 <!-- steps_sound&#45;&gt;has_red_spec -->
-<g id="edge41" class="edge">
+<g id="edge50" class="edge">
 <title>steps_sound&#45;&gt;has_red_spec</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M596.83,-417.33C621.52,-408.73 656.37,-396.59 682.91,-387.34"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="683.8,-389.26 688.78,-385.3 682.42,-385.29 683.8,-389.26"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M590.78,-466.97C610.01,-456.17 637.53,-441.1 662.21,-429 669.65,-425.35 677.74,-421.63 685.46,-418.2"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="686.64,-419.97 691.28,-415.63 684.94,-416.13 686.64,-419.97"/>
 </g>
 <!-- corpus_sound -->
-<g id="node47" class="node">
+<g id="node79" class="node">
 <title>corpus_sound</title>
-<g id="a_node47"><a xlink:title="corpus_sound theory/Tests.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="722.21" cy="-428" rx="43.1" ry="18"/>
-<text text-anchor="middle" x="722.21" y="-425.8" font-family="Inter" font-size="9.00" fill="#222222">corpus_sound</text>
+<g id="a_node79"><a xlink:title="corpus_sound theory/Tests.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="722.21" cy="-455" rx="43.1" ry="18"/>
+<text text-anchor="middle" x="722.21" y="-452.8" font-family="Inter" font-size="9.00" fill="#222222">corpus_sound</text>
 </a>
 </g>
 </g>
 <!-- steps_sound&#45;&gt;corpus_sound -->
-<g id="edge43" class="edge">
+<g id="edge59" class="edge">
 <title>steps_sound&#45;&gt;corpus_sound</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M604.52,-428C625.09,-428 650.65,-428 672.61,-428"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="672.7,-430.1 678.7,-428 672.7,-425.9 672.7,-430.1"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M602.55,-474.9C624.4,-471.24 652.39,-466.54 675.7,-462.63"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="676.26,-464.67 681.83,-461.6 675.57,-460.53 676.26,-464.67"/>
+</g>
+<!-- steps_sound_red1&#45;&gt;check_term_true -->
+<g id="edge31" class="edge">
+<title>steps_sound_red1&#45;&gt;check_term_true</title>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M756.97,-545.37C782.8,-534.95 818.46,-520.56 845.46,-509.66"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="846.31,-511.58 851.09,-507.39 844.74,-507.68 846.31,-511.58"/>
+</g>
+<!-- steps_sound_red1&#45;&gt;gen_fv_preserved -->
+<g id="edge36" class="edge">
+<title>steps_sound_red1&#45;&gt;gen_fv_preserved</title>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M774.6,-559C791.08,-559 809.44,-559 826.35,-559"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="826.51,-561.1 832.51,-559 826.51,-556.9 826.51,-561.1"/>
 </g>
 <!-- steps_sound_red1&#45;&gt;corpus_fv_preserved -->
-<g id="edge47" class="edge">
+<g id="edge63" class="edge">
 <title>steps_sound_red1&#45;&gt;corpus_fv_preserved</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M774.16,-480.32C788.35,-480.4 803.97,-480.5 818.86,-480.59"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="819.18,-482.7 825.2,-480.63 819.21,-478.5 819.18,-482.7"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M760.96,-571.19C783.94,-578.61 813.47,-588.15 837.87,-596.02"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="837.27,-598.04 843.63,-597.88 838.56,-594.04 837.27,-598.04"/>
 </g>
 <!-- positions_hole -->
-<g id="node38" class="node">
+<g id="node50" class="node">
 <title>positions_hole</title>
-<g id="a_node38"><a xlink:title="positions_hole theory/Reduction.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-312" rx="44.41" ry="18"/>
-<text text-anchor="middle" x="239.88" y="-309.8" font-family="Inter" font-size="9.00" fill="#222222">positions_hole</text>
+<g id="a_node50"><a xlink:title="positions_hole theory/Reduction.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-468" rx="44.41" ry="18"/>
+<text text-anchor="middle" x="239.88" y="-465.8" font-family="Inter" font-size="9.00" fill="#222222">positions_hole</text>
 </a>
 </g>
 </g>
 <!-- root_steps_in_steps -->
-<g id="node39" class="node">
+<g id="node51" class="node">
 <title>root_steps_in_steps</title>
-<g id="a_node39"><a xlink:title="root_steps_in_steps theory/Reduction.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-303" rx="56.66" ry="18"/>
-<text text-anchor="middle" x="408.74" y="-300.8" font-family="Inter" font-size="9.00" fill="#222222">root_steps_in_steps</text>
+<g id="a_node51"><a xlink:title="root_steps_in_steps theory/Reduction.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-468" rx="56.66" ry="18"/>
+<text text-anchor="middle" x="408.74" y="-465.8" font-family="Inter" font-size="9.00" fill="#222222">root_steps_in_steps</text>
 </a>
 </g>
 </g>
 <!-- positions_hole&#45;&gt;root_steps_in_steps -->
-<g id="edge33" class="edge">
+<g id="edge42" class="edge">
 <title>positions_hole&#45;&gt;root_steps_in_steps</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M284.28,-309.66C303.35,-308.63 326.08,-307.4 346.81,-306.29"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="347,-308.38 352.88,-305.96 346.78,-304.19 347,-308.38"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M284.72,-468C303.36,-468 325.43,-468 345.69,-468"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="345.92,-470.1 351.92,-468 345.92,-465.9 345.92,-470.1"/>
 </g>
 <!-- root_steps_in_steps&#45;&gt;steps_complete -->
-<g id="edge38" class="edge">
+<g id="edge47" class="edge">
 <title>root_steps_in_steps&#45;&gt;steps_complete</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M463.76,-307.55C479.43,-308.87 496.5,-310.3 512.06,-311.61"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="512.01,-313.71 518.16,-312.12 512.36,-309.53 512.01,-313.71"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M447.78,-454.87C455.01,-451.36 462.19,-447.1 468.21,-442 494.65,-419.62 490.02,-404.4 511.21,-377 521.23,-364.04 533.38,-350.38 543.53,-339.47"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="545.17,-340.79 547.74,-334.97 542.1,-337.92 545.17,-340.79"/>
 </g>
 <!-- plug_comp -->
-<g id="node40" class="node">
+<g id="node52" class="node">
 <title>plug_comp</title>
-<g id="a_node40"><a xlink:title="plug_comp theory/Reduction.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-199" rx="35.59" ry="18"/>
-<text text-anchor="middle" x="408.74" y="-196.8" font-family="Inter" font-size="9.00" fill="#222222">plug_comp</text>
+<g id="a_node52"><a xlink:title="plug_comp theory/Reduction.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-208" rx="35.59" ry="18"/>
+<text text-anchor="middle" x="408.74" y="-205.8" font-family="Inter" font-size="9.00" fill="#222222">plug_comp</text>
 </a>
 </g>
 </g>
 <!-- plug_comp&#45;&gt;steps_complete -->
-<g id="edge35" class="edge">
+<g id="edge44" class="edge">
 <title>plug_comp&#45;&gt;steps_complete</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M438.12,-209.33C448.02,-213.52 458.97,-218.83 468.21,-225 497.91,-244.83 526.96,-274.15 545.18,-294.12"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="543.77,-295.68 549.35,-298.73 546.88,-292.87 543.77,-295.68"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M437.98,-218.53C447.88,-222.74 458.85,-228.02 468.21,-234 496.59,-252.14 525.14,-278.38 543.63,-296.69"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="542.38,-298.41 548.11,-301.16 545.35,-295.44 542.38,-298.41"/>
 </g>
 <!-- positions_comp -->
-<g id="node41" class="node">
+<g id="node53" class="node">
 <title>positions_comp</title>
-<g id="a_node41"><a xlink:title="positions_comp theory/Reduction.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-355" rx="47.19" ry="18"/>
-<text text-anchor="middle" x="408.74" y="-352.8" font-family="Inter" font-size="9.00" fill="#222222">positions_comp</text>
+<g id="a_node53"><a xlink:title="positions_comp theory/Reduction.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-312" rx="47.19" ry="18"/>
+<text text-anchor="middle" x="408.74" y="-309.8" font-family="Inter" font-size="9.00" fill="#222222">positions_comp</text>
 </a>
 </g>
 </g>
 <!-- positions_comp&#45;&gt;steps_complete -->
-<g id="edge36" class="edge">
+<g id="edge45" class="edge">
 <title>positions_comp&#45;&gt;steps_complete</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M448.72,-345.16C470.13,-339.75 496.79,-333.02 519.1,-327.39"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="519.67,-329.41 524.97,-325.91 518.64,-325.34 519.67,-329.41"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M456.08,-313.8C473.49,-314.48 493.4,-315.25 511.35,-315.95"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="511.28,-318.05 517.36,-316.18 511.45,-313.85 511.28,-318.05"/>
 </g>
 <!-- at_ctx_comp -->
-<g id="node42" class="node">
+<g id="node54" class="node">
 <title>at_ctx_comp</title>
-<g id="a_node42"><a xlink:title="at_ctx_comp theory/Reduction.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-251" rx="40.33" ry="18"/>
-<text text-anchor="middle" x="408.74" y="-248.8" font-family="Inter" font-size="9.00" fill="#222222">at_ctx_comp</text>
+<g id="a_node54"><a xlink:title="at_ctx_comp theory/Reduction.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-260" rx="40.33" ry="18"/>
+<text text-anchor="middle" x="408.74" y="-257.8" font-family="Inter" font-size="9.00" fill="#222222">at_ctx_comp</text>
 </a>
 </g>
 </g>
 <!-- at_ctx_comp&#45;&gt;steps_complete -->
-<g id="edge34" class="edge">
+<g id="edge43" class="edge">
 <title>at_ctx_comp&#45;&gt;steps_complete</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M438.79,-263.23C463.76,-273.73 499.91,-288.94 526.99,-300.34"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="526.28,-302.32 532.62,-302.71 527.91,-298.45 526.28,-302.32"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M440.26,-271.46C464.53,-280.57 498.67,-293.39 524.98,-303.27"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="524.45,-305.32 530.81,-305.46 525.93,-301.38 524.45,-305.32"/>
+</g>
+<!-- steps_complete&#45;&gt;gen_complete -->
+<g id="edge34" class="edge">
+<title>steps_complete&#45;&gt;gen_complete</title>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M613.13,-320.12C631.78,-320.96 653.25,-321.93 672.11,-322.78"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="672.31,-324.89 678.4,-323.07 672.5,-320.7 672.31,-324.89"/>
 </g>
 <!-- steps_complete&#45;&gt;has_red_spec -->
-<g id="edge40" class="edge">
+<g id="edge49" class="edge">
 <title>steps_complete&#45;&gt;has_red_spec</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M599.84,-328.59C624.67,-337.88 658.46,-350.52 684.09,-360.11"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="683.4,-362.09 689.75,-362.23 684.87,-358.16 683.4,-362.09"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M593.2,-332.81C620.2,-347.61 661.68,-370.36 690.05,-385.92"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="689.27,-387.88 695.55,-388.93 691.29,-384.2 689.27,-387.88"/>
 </g>
 <!-- corpus_complete -->
-<g id="node48" class="node">
+<g id="node80" class="node">
 <title>corpus_complete</title>
-<g id="a_node48"><a xlink:title="corpus_complete theory/Tests.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="722.21" cy="-316" rx="51.27" ry="18"/>
-<text text-anchor="middle" x="722.21" y="-313.8" font-family="Inter" font-size="9.00" fill="#222222">corpus_complete</text>
+<g id="a_node80"><a xlink:title="corpus_complete theory/Tests.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="722.21" cy="-273" rx="51.27" ry="18"/>
+<text text-anchor="middle" x="722.21" y="-270.8" font-family="Inter" font-size="9.00" fill="#222222">corpus_complete</text>
 </a>
 </g>
 </g>
 <!-- steps_complete&#45;&gt;corpus_complete -->
-<g id="edge44" class="edge">
+<g id="edge60" class="edge">
 <title>steps_complete&#45;&gt;corpus_complete</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M613.13,-316C629.32,-316 647.63,-316 664.51,-316"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="664.66,-318.1 670.66,-316 664.66,-313.9 664.66,-318.1"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M603.73,-307.11C625.52,-300.78 653.13,-292.77 676.1,-286.1"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="676.96,-288.03 682.14,-284.34 675.79,-284 676.96,-288.03"/>
 </g>
 <!-- has_red_f -->
-<g id="node44" class="node">
+<g id="node56" class="node">
 <title>has_red_f</title>
-<g id="a_node44"><a xlink:title="has_red_f theory/Reduction.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="565.21" cy="-374" rx="32.16" ry="18"/>
-<text text-anchor="middle" x="565.21" y="-371.8" font-family="Inter" font-size="9.00" fill="#222222">has_red_f</text>
+<g id="a_node56"><a xlink:title="has_red_f theory/Reduction.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="565.21" cy="-403" rx="32.16" ry="18"/>
+<text text-anchor="middle" x="565.21" y="-400.8" font-family="Inter" font-size="9.00" fill="#222222">has_red_f</text>
 </a>
 </g>
 </g>
 <!-- has_red_f&#45;&gt;has_red_spec -->
-<g id="edge39" class="edge">
+<g id="edge48" class="edge">
 <title>has_red_f&#45;&gt;has_red_spec</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M597.57,-374C619.26,-374 648.54,-374 673.15,-374"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="673.31,-376.1 679.31,-374 673.31,-371.9 673.31,-376.1"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M597.57,-403C619.26,-403 648.54,-403 673.15,-403"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="673.31,-405.1 679.31,-403 673.31,-400.9 673.31,-405.1"/>
+</g>
+<!-- has_red_spec&#45;&gt;check_term_true -->
+<g id="edge30" class="edge">
+<title>has_red_spec&#45;&gt;check_term_true</title>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M753.64,-415.36C762.95,-419.42 773.12,-424.14 782.21,-429 796.39,-436.58 830.11,-458.35 854.92,-474.62"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="853.9,-476.46 860.07,-478 856.21,-472.95 853.9,-476.46"/>
 </g>
 <!-- red1_dec -->
-<g id="node46" class="node">
+<g id="node58" class="node">
 <title>red1_dec</title>
-<g id="a_node46"><a xlink:title="red1_dec theory/Reduction.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="885.25" cy="-374" rx="30.7" ry="18"/>
-<text text-anchor="middle" x="885.25" y="-371.8" font-family="Inter" font-size="9.00" fill="#222222">red1_dec</text>
+<g id="a_node58"><a xlink:title="red1_dec theory/Reduction.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="885.25" cy="-429" rx="30.7" ry="18"/>
+<text text-anchor="middle" x="885.25" y="-426.8" font-family="Inter" font-size="9.00" fill="#222222">red1_dec</text>
 </a>
 </g>
 </g>
 <!-- has_red_spec&#45;&gt;red1_dec -->
-<g id="edge42" class="edge">
+<g id="edge51" class="edge">
 <title>has_red_spec&#45;&gt;red1_dec</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M765.1,-374C790.96,-374 823.79,-374 848.43,-374"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="848.51,-376.1 854.51,-374 848.51,-371.9 848.51,-376.1"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M762.6,-409.36C789.24,-413.66 824.09,-419.29 849.65,-423.41"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="849.36,-425.49 855.61,-424.38 850.03,-421.35 849.36,-425.49"/>
 </g>
 <!-- corpus_decides -->
-<g id="node49" class="node">
+<g id="node81" class="node">
 <title>corpus_decides</title>
-<g id="a_node49"><a xlink:title="corpus_decides theory/Tests.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="885.25" cy="-426" rx="47.84" ry="18"/>
-<text text-anchor="middle" x="885.25" y="-423.8" font-family="Inter" font-size="9.00" fill="#222222">corpus_decides</text>
+<g id="a_node81"><a xlink:title="corpus_decides theory/Tests.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="885.25" cy="-377" rx="47.84" ry="18"/>
+<text text-anchor="middle" x="885.25" y="-374.8" font-family="Inter" font-size="9.00" fill="#222222">corpus_decides</text>
 </a>
 </g>
 </g>
 <!-- has_red_spec&#45;&gt;corpus_decides -->
-<g id="edge45" class="edge">
+<g id="edge61" class="edge">
 <title>has_red_spec&#45;&gt;corpus_decides</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M756.57,-384.77C781.5,-392.82 815.73,-403.88 842.48,-412.51"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="842.05,-414.58 848.41,-414.43 843.34,-410.58 842.05,-414.58"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M762.6,-396.64C784.4,-393.12 811.69,-388.71 834.9,-384.97"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="835.43,-387.01 841.02,-383.98 834.76,-382.86 835.43,-387.01"/>
+</g>
+<!-- open_rec_app -->
+<g id="node59" class="node">
+<title>open_rec_app</title>
+<g id="a_node59"><a xlink:title="open_rec_app theory/Substitution.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1144" rx="43.1" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-1141.8" font-family="Inter" font-size="9.00" fill="#222222">open_rec_app</text>
+</a>
+</g>
+</g>
+<!-- open_rec_lam -->
+<g id="node60" class="node">
+<title>open_rec_lam</title>
+<g id="a_node60"><a xlink:title="open_rec_lam theory/Substitution.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1196" rx="43.76" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-1193.8" font-family="Inter" font-size="9.00" fill="#222222">open_rec_lam</text>
+</a>
+</g>
+</g>
+<!-- open_rec_esub -->
+<g id="node61" class="node">
+<title>open_rec_esub</title>
+<g id="a_node61"><a xlink:title="open_rec_esub theory/Substitution.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1248" rx="46.38" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-1245.8" font-family="Inter" font-size="9.00" fill="#222222">open_rec_esub</text>
+</a>
+</g>
+</g>
+<!-- close_rec_app -->
+<g id="node62" class="node">
+<title>close_rec_app</title>
+<g id="a_node62"><a xlink:title="close_rec_app theory/Substitution.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1300" rx="44.41" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-1297.8" font-family="Inter" font-size="9.00" fill="#222222">close_rec_app</text>
+</a>
+</g>
+</g>
+<!-- close_rec_lam -->
+<g id="node63" class="node">
+<title>close_rec_lam</title>
+<g id="a_node63"><a xlink:title="close_rec_lam theory/Substitution.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1352" rx="44.41" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-1349.8" font-family="Inter" font-size="9.00" fill="#222222">close_rec_lam</text>
+</a>
+</g>
+</g>
+<!-- close_rec_esub -->
+<g id="node64" class="node">
+<title>close_rec_esub</title>
+<g id="a_node64"><a xlink:title="close_rec_esub theory/Substitution.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1404" rx="46.53" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-1401.8" font-family="Inter" font-size="9.00" fill="#222222">close_rec_esub</text>
+</a>
+</g>
+</g>
+<!-- subst_app -->
+<g id="node65" class="node">
+<title>subst_app</title>
+<g id="a_node65"><a xlink:title="subst_app theory/Substitution.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1456" rx="34.13" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-1453.8" font-family="Inter" font-size="9.00" fill="#222222">subst_app</text>
+</a>
+</g>
+</g>
+<!-- subst_lam -->
+<g id="node66" class="node">
+<title>subst_lam</title>
+<g id="a_node66"><a xlink:title="subst_lam theory/Substitution.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1508" rx="34.13" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-1505.8" font-family="Inter" font-size="9.00" fill="#222222">subst_lam</text>
+</a>
+</g>
+</g>
+<!-- subst_esub -->
+<g id="node67" class="node">
+<title>subst_esub</title>
+<g id="a_node67"><a xlink:title="subst_esub theory/Substitution.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1560" rx="36.25" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-1557.8" font-family="Inter" font-size="9.00" fill="#222222">subst_esub</text>
+</a>
+</g>
+</g>
+<!-- red_sub_root_to_red1 -->
+<g id="node71" class="node">
+<title>red_sub_root_to_red1</title>
+<g id="a_node71"><a xlink:title="red_sub_root_to_red1 theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1612" rx="60.09" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-1609.8" font-family="Inter" font-size="9.00" fill="#222222">red_sub_root_to_red1</text>
+</a>
+</g>
+</g>
+<!-- red_sub_to_red1 -->
+<g id="node72" class="node">
+<title>red_sub_to_red1</title>
+<g id="a_node72"><a xlink:title="red_sub_to_red1 theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-1612" rx="47.84" ry="18"/>
+<text text-anchor="middle" x="239.88" y="-1609.8" font-family="Inter" font-size="9.00" fill="#222222">red_sub_to_red1</text>
+</a>
+</g>
+</g>
+<!-- red_sub_root_to_red1&#45;&gt;red_sub_to_red1 -->
+<g id="edge56" class="edge">
+<title>red_sub_root_to_red1&#45;&gt;red_sub_to_red1</title>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M125.65,-1612C145.11,-1612 166.58,-1612 185.56,-1612"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="185.89,-1614.1 191.89,-1612 185.89,-1609.9 185.89,-1614.1"/>
+</g>
+<!-- red_sub_context -->
+<g id="node73" class="node">
+<title>red_sub_context</title>
+<g id="a_node73"><a xlink:title="red_sub_context theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1664" rx="49.15" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-1661.8" font-family="Inter" font-size="9.00" fill="#222222">red_sub_context</text>
+</a>
+</g>
+</g>
+<!-- red_sub_gc -->
+<g id="node74" class="node">
+<title>red_sub_gc</title>
+<g id="a_node74"><a xlink:title="red_sub_gc theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1716" rx="36.25" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-1713.8" font-family="Inter" font-size="9.00" fill="#222222">red_sub_gc</text>
+</a>
+</g>
+</g>
+<!-- red_sub_r -->
+<g id="node75" class="node">
+<title>red_sub_r</title>
+<g id="a_node75"><a xlink:title="red_sub_r theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1768" rx="32.82" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-1765.8" font-family="Inter" font-size="9.00" fill="#222222">red_sub_r</text>
+</a>
+</g>
+</g>
+<!-- occurs_zfill -->
+<g id="node76" class="node">
+<title>occurs_zfill</title>
+<g id="a_node76"><a xlink:title="occurs_zfill theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1820" rx="37.56" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-1817.8" font-family="Inter" font-size="9.00" fill="#222222">occurs_zfill</text>
+</a>
+</g>
+</g>
+<!-- zfill_occurs0 -->
+<g id="node77" class="node">
+<title>zfill_occurs0</title>
+<g id="a_node77"><a xlink:title="zfill_occurs0 theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-1820" rx="40.98" ry="18"/>
+<text text-anchor="middle" x="239.88" y="-1817.8" font-family="Inter" font-size="9.00" fill="#222222">zfill_occurs0</text>
+</a>
+</g>
+</g>
+<!-- occurs_zfill&#45;&gt;zfill_occurs0 -->
+<g id="edge57" class="edge">
+<title>occurs_zfill&#45;&gt;zfill_occurs0</title>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M102.85,-1820C128.98,-1820 164.34,-1820 192.45,-1820"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="192.7,-1822.1 198.7,-1820 192.7,-1817.9 192.7,-1822.1"/>
+</g>
+<!-- R_Gc_disjoint -->
+<g id="node78" class="node">
+<title>R_Gc_disjoint</title>
+<g id="a_node78"><a xlink:title="R_Gc_disjoint theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-1820" rx="41.64" ry="18"/>
+<text text-anchor="middle" x="408.74" y="-1817.8" font-family="Inter" font-size="9.00" fill="#222222">R_Gc_disjoint</text>
+</a>
+</g>
+</g>
+<!-- zfill_occurs0&#45;&gt;R_Gc_disjoint -->
+<g id="edge58" class="edge">
+<title>zfill_occurs0&#45;&gt;R_Gc_disjoint</title>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M281.27,-1820C305.28,-1820 335.83,-1820 360.89,-1820"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="361.14,-1822.1 367.14,-1820 361.14,-1817.9 361.14,-1822.1"/>
 </g>
 </g>
 </svg>
diff --git a/graphs/theorems.json b/graphs/theorems.json
index 5f664a4..d0844ea 100644
--- a/graphs/theorems.json
+++ b/graphs/theorems.json
@@ -9,6 +9,7 @@
     "html": "https://arxiv.org/html/2312.13270v1"
   },
   "milestones": [
+    "M0",
     "M1",
     "M2"
   ],
@@ -356,6 +357,142 @@
         "lemma_2_2_full_comp"
       ]
     },
+    {
+      "id": "par_red1_iff",
+      "label": "par_red1_iff",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M0",
+      "section": "",
+      "file": "theory/Parallel.v",
+      "depends": []
+    },
+    {
+      "id": "red1_in_par",
+      "label": "red1_in_par",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M0",
+      "section": "",
+      "file": "theory/Parallel.v",
+      "depends": []
+    },
+    {
+      "id": "par_context",
+      "label": "par_context",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M0",
+      "section": "",
+      "file": "theory/Parallel.v",
+      "depends": []
+    },
+    {
+      "id": "par_to_red1_or_eq",
+      "label": "par_to_red1_or_eq",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M0",
+      "section": "",
+      "file": "theory/Parallel.v",
+      "depends": [
+        "par_red1_iff"
+      ]
+    },
+    {
+      "id": "red1_or_eq_to_par",
+      "label": "red1_or_eq_to_par",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M0",
+      "section": "",
+      "file": "theory/Parallel.v",
+      "depends": [
+        "par_red1_iff"
+      ]
+    },
+    {
+      "id": "par_reflexive",
+      "label": "par_reflexive",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M0",
+      "section": "",
+      "file": "theory/Parallel.v",
+      "depends": []
+    },
+    {
+      "id": "gen_list_length",
+      "label": "gen_list_length",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M0",
+      "section": "",
+      "file": "theory/Random.v",
+      "depends": []
+    },
+    {
+      "id": "check_term_true",
+      "label": "check_term_true",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M0",
+      "section": "",
+      "file": "theory/Random.v",
+      "depends": [
+        "has_red_spec",
+        "steps_sound_red1"
+      ]
+    },
+    {
+      "id": "check_all_true",
+      "label": "check_all_true",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M0",
+      "section": "",
+      "file": "theory/Random.v",
+      "depends": [
+        "check_term_true"
+      ]
+    },
+    {
+      "id": "gen_sound",
+      "label": "gen_sound",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M0",
+      "section": "",
+      "file": "theory/Random.v",
+      "depends": [
+        "steps_sound"
+      ]
+    },
+    {
+      "id": "gen_complete",
+      "label": "gen_complete",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M0",
+      "section": "",
+      "file": "theory/Random.v",
+      "depends": [
+        "steps_complete"
+      ]
+    },
+    {
+      "id": "gen_fv_preserved",
+      "label": "gen_fv_preserved",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M0",
+      "section": "",
+      "file": "theory/Random.v",
+      "depends": [
+        "lemma_2_1_fv_preserved",
+        "steps_sound_red1"
+      ]
+    },
     {
       "id": "zdecs_sound",
       "label": "zdecs_sound",
@@ -539,6 +676,219 @@
         "has_red_spec"
       ]
     },
+    {
+      "id": "open_rec_app",
+      "label": "open_rec_app",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M0",
+      "section": "",
+      "file": "theory/Substitution.v",
+      "depends": []
+    },
+    {
+      "id": "open_rec_lam",
+      "label": "open_rec_lam",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M0",
+      "section": "",
+      "file": "theory/Substitution.v",
+      "depends": []
+    },
+    {
+      "id": "open_rec_esub",
+      "label": "open_rec_esub",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M0",
+      "section": "",
+      "file": "theory/Substitution.v",
+      "depends": []
+    },
+    {
+      "id": "close_rec_app",
+      "label": "close_rec_app",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M0",
+      "section": "",
+      "file": "theory/Substitution.v",
+      "depends": []
+    },
+    {
+      "id": "close_rec_lam",
+      "label": "close_rec_lam",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M0",
+      "section": "",
+      "file": "theory/Substitution.v",
+      "depends": []
+    },
+    {
+      "id": "close_rec_esub",
+      "label": "close_rec_esub",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M0",
+      "section": "",
+      "file": "theory/Substitution.v",
+      "depends": []
+    },
+    {
+      "id": "subst_app",
+      "label": "subst_app",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M0",
+      "section": "",
+      "file": "theory/Substitution.v",
+      "depends": []
+    },
+    {
+      "id": "subst_lam",
+      "label": "subst_lam",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M0",
+      "section": "",
+      "file": "theory/Substitution.v",
+      "depends": []
+    },
+    {
+      "id": "subst_esub",
+      "label": "subst_esub",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M0",
+      "section": "",
+      "file": "theory/Substitution.v",
+      "depends": []
+    },
+    {
+      "id": "subst_notin",
+      "label": "subst_notin",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M0",
+      "section": "",
+      "file": "theory/Substitution.v",
+      "depends": [
+        "close_rec_notin",
+        "open_rec_occurs_false"
+      ]
+    },
+    {
+      "id": "subst_lc_self",
+      "label": "subst_lc_self",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M0",
+      "section": "",
+      "file": "theory/Substitution.v",
+      "depends": [
+        "subst_fvar_self"
+      ]
+    },
+    {
+      "id": "subst_other",
+      "label": "subst_other",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M0",
+      "section": "",
+      "file": "theory/Substitution.v",
+      "depends": [
+        "subst_fvar_other"
+      ]
+    },
+    {
+      "id": "red_sub_root_to_red1",
+      "label": "red_sub_root_to_red1",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M0",
+      "section": "",
+      "file": "theory/Subsystem.v",
+      "depends": []
+    },
+    {
+      "id": "red_sub_to_red1",
+      "label": "red_sub_to_red1",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M0",
+      "section": "",
+      "file": "theory/Subsystem.v",
+      "depends": [
+        "red_sub_root_to_red1"
+      ]
+    },
+    {
+      "id": "red_sub_context",
+      "label": "red_sub_context",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M0",
+      "section": "",
+      "file": "theory/Subsystem.v",
+      "depends": []
+    },
+    {
+      "id": "red_sub_gc",
+      "label": "red_sub_gc",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M0",
+      "section": "",
+      "file": "theory/Subsystem.v",
+      "depends": []
+    },
+    {
+      "id": "red_sub_r",
+      "label": "red_sub_r",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M0",
+      "section": "",
+      "file": "theory/Subsystem.v",
+      "depends": []
+    },
+    {
+      "id": "occurs_zfill",
+      "label": "occurs_zfill",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M0",
+      "section": "",
+      "file": "theory/Subsystem.v",
+      "depends": []
+    },
+    {
+      "id": "zfill_occurs0",
+      "label": "zfill_occurs0",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M0",
+      "section": "",
+      "file": "theory/Subsystem.v",
+      "depends": [
+        "occurs_zfill"
+      ]
+    },
+    {
+      "id": "R_Gc_disjoint",
+      "label": "R_Gc_disjoint",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M0",
+      "section": "",
+      "file": "theory/Subsystem.v",
+      "depends": [
+        "zfill_occurs0"
+      ]
+    },
     {
       "id": "corpus_sound",
       "label": "corpus_sound",
diff --git a/scripts/audit.sh b/scripts/audit.sh
index 4728d89..e4a5ec5 100755
--- a/scripts/audit.sh
+++ b/scripts/audit.sh
@@ -35,7 +35,7 @@ done < <(find theory -name '*.v' -print0 2>/dev/null)
 echo "== Print Assumptions =="
 WORK="$(mktemp -d ./.audit-work.XXXXXX)"
 cp theory/*.v "$WORK"/
-for f in ExecReducer Binding Reduction Metatheory Subsystem Substitution Parallel Tests; do
+for f in ExecReducer Binding Reduction Metatheory Subsystem Substitution Parallel Tests Random; do
   echo "-- $f"
   out="$(rocq compile -Q "$WORK" LambdaSub "$WORK/$f.v" 2>&1 || true)"
   echo "$out"
diff --git a/scripts/samplecheck.sh b/scripts/samplecheck.sh
new file mode 100755
index 0000000..3c661e8
--- /dev/null
+++ b/scripts/samplecheck.sh
@@ -0,0 +1,19 @@
+#!/usr/bin/env bash
+set -euo pipefail
+ROOT="$(cd "$(dirname "$0")/.." && pwd)"
+cd "$ROOT"
+
+if ! command -v rocq >/dev/null 2>&1; then
+  if command -v opam >/dev/null 2>&1; then
+    eval "$(opam env --switch=rocq-system --set-switch 2>/dev/null || true)"
+  fi
+fi
+
+if ! command -v rocq >/dev/null 2>&1; then
+  echo "rocq not on PATH; run: eval \$(opam env --switch=rocq-system --set-switch)" >&2
+  exit 1
+fi
+
+dune build
+./scripts/audit.sh
+echo "SAMPLE CHECK OK: 16 generated terms checked against red1 by theory/Random.v"
diff --git a/theory/Random.v b/theory/Random.v
new file mode 100644
index 0000000..f615b43
--- /dev/null
+++ b/theory/Random.v
@@ -0,0 +1,85 @@
+From Stdlib Require Import List Bool Arith Lia PeanoNat.
+Import ListNotations.
+From LambdaSub Require Import ExecReducer Binding Reduction Metatheory Subsystem Substitution Parallel.
+
+Definition next (s : nat) : nat := (s * 3 + 1) mod 97.
+
+Fixpoint gen (fuel : nat) (s : nat) : trm * nat :=
+  match fuel with
+  | 0 => (FVar (s mod 5), next s)
+  | S f =>
+    match next s mod 6 with
+    | 0 => (FVar (next s mod 5), next (next s))
+    | 1 => let (a, s1) := gen f (next s) in
+           let (b, s2) := gen f s1 in (App a b, next s2)
+    | 2 => let (a, s1) := gen f (next s) in (Lam a, next s1)
+    | 3 => let (a, s1) := gen f (next s) in
+           let (b, s2) := gen f s1 in (ESub a b, next s2)
+    | 4 => (BVar (next s mod 3), next (next s))
+    | _ => (FVar (next s mod 5), next (next s))
+    end
+  end.
+
+Fixpoint gen_list (count : nat) (s : nat) : list trm :=
+  match count with
+  | 0 => []
+  | S c => let (t, s') := gen 3 s in t :: gen_list c s'
+  end.
+
+Lemma gen_list_length : forall count s, length (gen_list count s) = count.
+Proof.
+  induction count; intros s.
+  - reflexivity.
+  - cbn [gen_list].
+    destruct (gen 3 s) as [t s'].
+    cbn [length].
+    rewrite IHcount. reflexivity.
+Qed.
+
+Definition check_term (t : trm) : bool :=
+  forallb (fun p => has_red t (snd p)) (steps t).
+
+Definition check_all (l : list trm) : bool := forallb check_term l.
+
+Lemma check_term_true : forall t, check_term t = true.
+Proof.
+  intros t. unfold check_term.
+  apply forallb_forall. intros [r s] Hp.
+  apply has_red_spec. exact (steps_sound_red1 t r s Hp).
+Qed.
+
+Lemma check_all_true : forall l, check_all l = true.
+Proof.
+  intros l. unfold check_all.
+  apply forallb_forall. intros t _. apply check_term_true.
+Qed.
+
+Example sample_agreement : check_all (gen_list 16 7) = true.
+Proof. apply check_all_true. Qed.
+
+Example sample_length : length (gen_list 16 7) = 16.
+Proof. apply gen_list_length. Qed.
+
+Lemma gen_sound : forall count seed t, In t (gen_list count seed) ->
+  forall p, In p (steps t) -> red1r (fst p) t (snd p).
+Proof. intros count seed t _ [r s] Hp. apply steps_sound. exact Hp. Qed.
+
+Lemma gen_complete : forall count seed t r t', In t (gen_list count seed) ->
+  red1r r t t' -> In (r,t') (steps t).
+Proof. intros count seed t r t' _ H. apply steps_complete. exact H. Qed.
+
+Lemma gen_fv_preserved : forall count seed t p, In t (gen_list count seed) ->
+  In p (steps t) -> incl (fvs (snd p)) (fvs t).
+Proof.
+  intros count seed t [r s] _ H. simpl.
+  apply (lemma_2_1_fv_preserved t s). exact (steps_sound_red1 t r s H).
+Qed.
+
+Print Assumptions gen_list_length.
+Print Assumptions check_term_true.
+Print Assumptions check_all_true.
+Print Assumptions sample_agreement.
+Print Assumptions sample_length.
+Print Assumptions gen_sound.
+Print Assumptions gen_complete.
+Print Assumptions gen_fv_preserved.