diff --git a/graphs/dependency.dot b/graphs/dependency.dot
index 4708428..f75a20f 100644
--- a/graphs/dependency.dot
+++ b/graphs/dependency.dot
@@ -49,6 +49,9 @@ digraph theorem_deps {
   mred_B_intro [label="mred_B_intro", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="mred_B_intro theory/Metaterm.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
   mred_gc_intro [label="mred_gc_intro", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="mred_gc_intro theory/Metaterm.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
   mred_r_intro [label="mred_r_intro", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="mred_r_intro theory/Metaterm.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  Plus_mred_of_Plus_red1 [label="Plus_mred_of_Plus_red1", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="Plus_mred_of_Plus_red1 theory/Metaterm.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  mred_full_comp_pure [label="mred_full_comp_pure", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="mred_full_comp_pure theory/Metaterm.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  mred_plus_one [label="mred_plus_one", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="mred_plus_one theory/Metaterm.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
   Plus_red1_context [label="Plus_red1_context", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="Plus_red1_context theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
   occurs_count_zero [label="occurs_count_zero", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="occurs_count_zero theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
   occurs_count_false [label="occurs_count_false", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="occurs_count_false theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
@@ -70,6 +73,8 @@ digraph theorem_deps {
   isubst_meta_in [label="isubst_meta_in", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="isubst_meta_in theory/NamedMeta.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
   isubst_meta_notin [label="isubst_meta_notin", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="isubst_meta_notin theory/NamedMeta.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
   eqC_in_Es [label="eqC_in_Es", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="eqC_in_Es theory/NamedMeta.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  Es_ctx_any [label="Es_ctx_any", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="Es_ctx_any theory/NamedMeta.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  nred_R_intro [label="nred_R_intro", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="nred_R_intro theory/NamedMeta.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
   Es_refl_any [label="Es_refl_any", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="Es_refl_any theory/NamedMeta.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
   Es_sym_any [label="Es_sym_any", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="Es_sym_any theory/NamedMeta.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
   Es_trans_any [label="Es_trans_any", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="Es_trans_any theory/NamedMeta.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
@@ -155,6 +160,8 @@ digraph theorem_deps {
   mfvs_lift_m -> mfvs_open_m;
   of_trm_plug -> mred_term_context;
   of_trm_moccurs -> of_trm_moccurs0;
+  Plus_mred_of_Plus_red1 -> mred_full_comp_pure;
+  lemma_2_2_full_comp -> mred_full_comp_pure;
   occurs_count_zero -> occurs_count_pos;
   occurs_count_false -> occurs_count_zfill_plug;
   occurs_lift_self -> occurs_count_zfill_plug;
diff --git a/graphs/dependency.png b/graphs/dependency.png
index eace39f..e52f959 100644
Binary files a/graphs/dependency.png and b/graphs/dependency.png differ
diff --git a/graphs/dependency.svg b/graphs/dependency.svg
index 72ccbcc..aa208d0 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="1294pt" height="3600pt"
- viewBox="0.00 0.00 1293.96 3600.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 3596)">
+<svg width="1296pt" height="3718pt"
+ viewBox="0.00 0.00 1296.27 3718.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 3714)">
 <title>theorem_deps</title>
-<polygon fill="white" stroke="transparent" points="-4,4 -4,-3596 1289.96,-3596 1289.96,4 -4,4"/>
-<text text-anchor="start" x="406.48" y="-3579.4" font-family="Inter" font-weight="bold" font-size="12.00">Milner&#39;s Lambda&#45;Calculus with Partial Substitutions &#45; theorem dependency (M4)</text>
-<text text-anchor="start" x="569.98" y="-3569.8" font-family="Inter" font-size="9.00" fill="#38761d">proved</text>
-<text text-anchor="start" x="599.98" y="-3569.8" font-family="Inter" font-size="9.00"> &#160;&#160;</text>
-<text text-anchor="start" x="606.98" y="-3569.8" font-family="Inter" font-size="9.00" fill="#b45f06">stated</text>
-<text text-anchor="start" x="633.98" y="-3569.8" font-family="Inter" font-size="9.00"> &#160;&#160;</text>
-<text text-anchor="start" x="640.98" y="-3569.8" font-family="Inter" font-size="9.00" fill="#777777">planned</text>
-<text text-anchor="start" x="674.98" y="-3569.8" font-family="Inter" font-size="9.00"> &#160;&#160;</text>
-<text text-anchor="start" x="681.98" y="-3569.8" font-family="Inter" font-size="9.00" fill="#cc0000">blocked</text>
+<polygon fill="white" stroke="transparent" points="-4,4 -4,-3714 1292.27,-3714 1292.27,4 -4,4"/>
+<text text-anchor="start" x="407.63" y="-3697.4" font-family="Inter" font-weight="bold" font-size="12.00">Milner&#39;s Lambda&#45;Calculus with Partial Substitutions &#45; theorem dependency (M4)</text>
+<text text-anchor="start" x="571.13" y="-3687.8" font-family="Inter" font-size="9.00" fill="#38761d">proved</text>
+<text text-anchor="start" x="601.13" y="-3687.8" font-family="Inter" font-size="9.00"> &#160;&#160;</text>
+<text text-anchor="start" x="608.13" y="-3687.8" font-family="Inter" font-size="9.00" fill="#b45f06">stated</text>
+<text text-anchor="start" x="635.13" y="-3687.8" font-family="Inter" font-size="9.00"> &#160;&#160;</text>
+<text text-anchor="start" x="642.13" y="-3687.8" font-family="Inter" font-size="9.00" fill="#777777">planned</text>
+<text text-anchor="start" x="676.13" y="-3687.8" font-family="Inter" font-size="9.00"> &#160;&#160;</text>
+<text text-anchor="start" x="683.13" y="-3687.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="-893" rx="27" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-890.8" font-family="Inter" font-size="9.00" fill="#222222">fvs_lift</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-855" rx="27" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-852.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="-945" rx="41.64" ry="18"/>
-<text text-anchor="middle" x="239.88" y="-942.8" font-family="Inter" font-size="9.00" fill="#222222">open_rec_fvs</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-907" rx="41.64" ry="18"/>
+<text text-anchor="middle" x="239.88" y="-904.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,-900.23C118.42,-908.72 165.55,-922.91 199.19,-933.04"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="198.95,-935.17 205.3,-934.89 200.16,-931.15 198.95,-935.17"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M90.24,-862.23C118.42,-870.72 165.55,-884.91 199.19,-895.04"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="198.95,-897.17 205.3,-896.89 200.16,-893.15 198.95,-897.17"/>
 </g>
 <!-- fvs_zplug_lift -->
-<g id="node53" class="node">
+<g id="node56" class="node">
 <title>fvs_zplug_lift</title>
-<g id="a_node53"><a xlink:title="fvs_zplug_lift theory/Metatheory.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-893" rx="40.98" ry="18"/>
-<text text-anchor="middle" x="239.88" y="-890.8" font-family="Inter" font-size="9.00" fill="#222222">fvs_zplug_lift</text>
+<g id="a_node56"><a xlink:title="fvs_zplug_lift theory/Metatheory.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-855" rx="40.98" ry="18"/>
+<text text-anchor="middle" x="239.88" y="-852.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="edge30" class="edge">
+<g id="edge32" class="edge">
 <title>fvs_lift&#45;&gt;fvs_zplug_lift</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M92.46,-893C118.9,-893 160.28,-893 192.31,-893"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="192.58,-895.1 198.58,-893 192.58,-890.9 192.58,-895.1"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M92.46,-855C118.9,-855 160.28,-855 192.31,-855"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="192.58,-857.1 198.58,-855 192.58,-852.9 192.58,-857.1"/>
 </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="-1049" rx="27" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-1046.8" font-family="Inter" font-size="9.00" fill="#222222">lift_lc</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1011" rx="27" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-1008.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="-1049" rx="27.93" ry="18"/>
-<text text-anchor="middle" x="239.88" y="-1046.8" font-family="Inter" font-size="9.00" fill="#222222">lift_0_lc</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-1011" rx="27.93" ry="18"/>
+<text text-anchor="middle" x="239.88" y="-1008.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,-1049C122.79,-1049 172.78,-1049 205.77,-1049"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="206.13,-1051.1 212.13,-1049 206.13,-1046.9 206.13,-1051.1"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M92.46,-1011C122.79,-1011 172.78,-1011 205.77,-1011"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="206.13,-1013.1 212.13,-1011 206.13,-1008.9 206.13,-1013.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="-1049" rx="45.72" ry="18"/>
-<text text-anchor="middle" x="408.74" y="-1046.8" font-family="Inter" font-size="9.00" fill="#222222">subst_fvar_self</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-1011" rx="45.72" ry="18"/>
+<text text-anchor="middle" x="408.74" y="-1008.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,-1049C291.68,-1049 327.51,-1049 356.92,-1049"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="357.09,-1051.1 363.09,-1049 357.09,-1046.9 357.09,-1051.1"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M267.69,-1011C291.68,-1011 327.51,-1011 356.92,-1011"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="357.09,-1013.1 363.09,-1011 357.09,-1008.9 357.09,-1013.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="-841" rx="46.38" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-838.8" font-family="Inter" font-size="9.00" fill="#222222">open_rec_bvar</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-803" rx="46.38" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-800.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,-851.95C111.91,-855.83 122.04,-860.81 130.48,-867 154.67,-884.72 149.23,-901.35 173.48,-919 181.18,-924.6 190.25,-929.2 199.15,-932.89"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="198.6,-934.94 204.95,-935.19 200.14,-931.03 198.6,-934.94"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M102.23,-813.95C111.91,-817.83 122.04,-822.81 130.48,-829 154.67,-846.72 149.23,-863.35 173.48,-881 181.18,-886.6 190.25,-891.2 199.15,-894.89"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="198.6,-896.94 204.95,-897.19 200.14,-893.03 198.6,-896.94"/>
 </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="-841" rx="36.9" ry="18"/>
-<text text-anchor="middle" x="239.88" y="-838.8" font-family="Inter" font-size="9.00" fill="#222222">open_close</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-803" rx="36.9" ry="18"/>
+<text text-anchor="middle" x="239.88" y="-800.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,-841C137.96,-841 170.95,-841 196.74,-841"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="196.79,-843.1 202.79,-841 196.79,-838.9 196.79,-843.1"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M111.6,-803C137.96,-803 170.95,-803 196.74,-803"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="196.79,-805.1 202.79,-803 196.79,-800.9 196.79,-805.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="-1101" rx="45.07" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-1098.8" font-family="Inter" font-size="9.00" fill="#222222">close_rec_fvar</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1063" rx="45.07" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-1060.8" font-family="Inter" font-size="9.00" fill="#222222">close_rec_fvar</text>
 </a>
 </g>
 </g>
@@ -138,70 +138,70 @@
 <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="-187" rx="65.48" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-184.8" font-family="Inter" font-size="9.00" fill="#222222">open_rec_occurs_false</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-238" rx="65.48" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-235.8" font-family="Inter" font-size="9.00" fill="#222222">open_rec_occurs_false</text>
 </a>
 </g>
 </g>
 <!-- open_rec_zplug_lift -->
-<g id="node50" class="node">
+<g id="node53" class="node">
 <title>open_rec_zplug_lift</title>
-<g id="a_node50"><a xlink:title="open_rec_zplug_lift theory/Metatheory.v https://arxiv.org/html/2312.13270v1">
+<g id="a_node53"><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="-260" rx="56.66" ry="18"/>
 <text text-anchor="middle" x="239.88" y="-257.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="edge22" class="edge">
+<g id="edge24" class="edge">
 <title>open_rec_occurs_false&#45;&gt;open_rec_zplug_lift</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M100.4,-202.33C121.4,-211.67 148.91,-223.73 173.48,-234 181.21,-237.23 189.48,-240.59 197.46,-243.78"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="197.14,-245.92 203.49,-246.19 198.69,-242.02 197.14,-245.92"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M124.69,-245.45C142.88,-247.77 162.92,-250.32 181.07,-252.63"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="180.93,-254.73 187.15,-253.41 181.46,-250.57 180.93,-254.73"/>
 </g>
 <!-- full_comp_aux -->
-<g id="node51" class="node">
+<g id="node54" class="node">
 <title>full_comp_aux</title>
-<g id="a_node51"><a xlink:title="full_comp_aux theory/Metatheory.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-355" rx="44.41" ry="18"/>
-<text text-anchor="middle" x="408.74" y="-352.8" font-family="Inter" font-size="9.00" fill="#222222">full_comp_aux</text>
+<g id="a_node54"><a xlink:title="full_comp_aux theory/Metatheory.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-353" rx="44.41" ry="18"/>
+<text text-anchor="middle" x="408.74" y="-350.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="edge25" class="edge">
+<g id="edge27" class="edge">
 <title>open_rec_occurs_false&#45;&gt;full_comp_aux</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M72.91,-204.91C86.26,-237.92 119.69,-307.71 173.48,-338 231.75,-370.81 311.49,-368.56 361.29,-362.71"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="361.81,-364.76 367.51,-361.94 361.29,-360.59 361.81,-364.76"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M87.92,-255.13C100.64,-265.45 116.85,-279.06 130.48,-292 150.78,-311.26 148.18,-326.04 173.48,-338 233.2,-366.22 311.19,-364.72 360.39,-359.82"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="360.79,-361.89 366.54,-359.18 360.35,-357.71 360.79,-361.89"/>
 </g>
 <!-- subst_notin -->
-<g id="node107" class="node">
+<g id="node112" class="node">
 <title>subst_notin</title>
-<g id="a_node107"><a xlink:title="subst_notin theory/Substitution.v https://arxiv.org/html/2312.13270v1">
+<g id="a_node112"><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="edge66" class="edge">
+<g id="edge68" class="edge">
 <title>open_rec_occurs_false&#45;&gt;subst_notin</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M75.37,-169.12C91.41,-139.31 127.39,-79.25 173.48,-44 181.6,-37.79 191.39,-32.87 200.9,-29.05"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="201.91,-30.91 206.77,-26.81 200.41,-26.98 201.91,-30.91"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M71.64,-219.82C83.75,-181.98 116.59,-94.11 173.48,-44 181.15,-37.25 190.79,-32.13 200.29,-28.3"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="201.3,-30.17 206.17,-26.08 199.82,-26.24 201.3,-30.17"/>
 </g>
 <!-- full_comp_aux_sub -->
-<g id="node121" class="node">
+<g id="node126" class="node">
 <title>full_comp_aux_sub</title>
-<g id="a_node121"><a xlink:title="full_comp_aux_sub theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-257" rx="54.7" ry="18"/>
-<text text-anchor="middle" x="408.74" y="-254.8" font-family="Inter" font-size="9.00" fill="#222222">full_comp_aux_sub</text>
+<g id="a_node126"><a xlink:title="full_comp_aux_sub theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-217" rx="54.7" ry="18"/>
+<text text-anchor="middle" x="408.74" y="-214.8" font-family="Inter" font-size="9.00" fill="#222222">full_comp_aux_sub</text>
 </a>
 </g>
 </g>
 <!-- open_rec_occurs_false&#45;&gt;full_comp_aux_sub -->
-<g id="edge76" class="edge">
+<g id="edge78" class="edge">
 <title>open_rec_occurs_false&#45;&gt;full_comp_aux_sub</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M89.81,-170.29C135.38,-140.25 237.14,-84.29 306.27,-130 346.97,-156.91 315.05,-196.23 349.27,-231 353.28,-235.07 358.03,-238.55 363.07,-241.52"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="362.36,-243.53 368.63,-244.55 364.37,-239.84 362.36,-243.53"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M129.27,-234.12C191.88,-230.27 287.14,-224.42 348.41,-220.65"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="348.74,-222.73 354.6,-220.27 348.48,-218.54 348.74,-222.73"/>
 </g>
 <!-- close_rec_notin -->
 <g id="node7" class="node">
@@ -213,7 +213,7 @@
 </g>
 </g>
 <!-- close_rec_notin&#45;&gt;subst_notin -->
-<g id="edge65" class="edge">
+<g id="edge67" 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"/>
@@ -222,8 +222,8 @@
 <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="-997" rx="42.95" ry="18"/>
-<text text-anchor="middle" x="239.88" y="-994.8" font-family="Inter" font-size="9.00" fill="#222222">close_rec_fvs</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-959" rx="42.95" ry="18"/>
+<text text-anchor="middle" x="239.88" y="-956.8" font-family="Inter" font-size="9.00" fill="#222222">close_rec_fvs</text>
 </a>
 </g>
 </g>
@@ -231,83 +231,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="-997" rx="32.16" ry="18"/>
-<text text-anchor="middle" x="408.74" y="-994.8" font-family="Inter" font-size="9.00" fill="#222222">subst_fvs</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-959" rx="32.16" ry="18"/>
+<text text-anchor="middle" x="408.74" y="-956.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,-997C309.8,-997 344.23,-997 370.13,-997"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="370.18,-999.1 376.18,-997 370.18,-994.9 370.18,-999.1"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M282.98,-959C309.8,-959 344.23,-959 370.13,-959"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="370.18,-961.1 376.18,-959 370.18,-956.9 370.18,-961.1"/>
 </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="-945" rx="57.97" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-942.8" font-family="Inter" font-size="9.00" fill="#222222">open_rec_bvar_neq</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-907" rx="57.97" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-904.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,-945C145.5,-945 170.71,-945 191.9,-945"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="192.05,-947.1 198.05,-945 192.05,-942.9 192.05,-947.1"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M123.25,-907C145.5,-907 170.71,-907 191.9,-907"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="192.05,-909.1 198.05,-907 192.05,-904.9 192.05,-909.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,-955.4C303.28,-964.45 345.15,-977.49 374.23,-986.56"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="373.87,-988.65 380.23,-988.43 375.12,-984.64 373.87,-988.65"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M274.24,-917.4C303.28,-926.45 345.15,-939.49 374.23,-948.56"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="373.87,-950.65 380.23,-950.43 375.12,-946.64 373.87,-950.65"/>
 </g>
 <!-- subst_lc_self -->
-<g id="node108" class="node">
+<g id="node113" class="node">
 <title>subst_lc_self</title>
-<g id="a_node108"><a xlink:title="subst_lc_self theory/Substitution.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="577.6" cy="-1049" rx="40.33" ry="18"/>
-<text text-anchor="middle" x="577.6" y="-1046.8" font-family="Inter" font-size="9.00" fill="#222222">subst_lc_self</text>
+<g id="a_node113"><a xlink:title="subst_lc_self theory/Substitution.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="578.76" cy="-1011" rx="40.33" ry="18"/>
+<text text-anchor="middle" x="578.76" y="-1008.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="edge67" class="edge">
+<g id="edge69" class="edge">
 <title>subst_fvar_self&#45;&gt;subst_lc_self</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M454.45,-1049C478.12,-1049 507.11,-1049 530.92,-1049"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="531.17,-1051.1 537.17,-1049 531.17,-1046.9 531.17,-1051.1"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M454.76,-1011C478.68,-1011 508.01,-1011 532.03,-1011"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="532.33,-1013.1 538.33,-1011 532.33,-1008.9 532.33,-1013.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="-1153" rx="49.8" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-1150.8" font-family="Inter" font-size="9.00" fill="#222222">subst_fvar_other</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1115" rx="49.8" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-1112.8" font-family="Inter" font-size="9.00" fill="#222222">subst_fvar_other</text>
 </a>
 </g>
 </g>
 <!-- subst_other -->
-<g id="node109" class="node">
+<g id="node114" class="node">
 <title>subst_other</title>
-<g id="a_node109"><a xlink:title="subst_other theory/Substitution.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-1153" rx="37.56" ry="18"/>
-<text text-anchor="middle" x="239.88" y="-1150.8" font-family="Inter" font-size="9.00" fill="#222222">subst_other</text>
+<g id="a_node114"><a xlink:title="subst_other theory/Substitution.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-1115" rx="37.56" ry="18"/>
+<text text-anchor="middle" x="239.88" y="-1112.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="edge68" class="edge">
+<g id="edge70" class="edge">
 <title>subst_fvar_other&#45;&gt;subst_other</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M115.25,-1153C140.7,-1153 171.52,-1153 196.02,-1153"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="196.1,-1155.1 202.1,-1153 196.1,-1150.9 196.1,-1155.1"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M115.25,-1115C140.7,-1115 171.52,-1115 196.02,-1115"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="196.1,-1117.1 202.1,-1115 196.1,-1112.9 196.1,-1117.1"/>
 </g>
 <!-- Star_trans -->
 <g id="node15" class="node">
 <title>Star_trans</title>
 <g id="a_node15"><a xlink:title="Star_trans theory/Closure.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1205" rx="34.78" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-1202.8" font-family="Inter" font-size="9.00" fill="#222222">Star_trans</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1167" rx="34.78" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-1164.8" font-family="Inter" font-size="9.00" fill="#222222">Star_trans</text>
 </a>
 </g>
 </g>
@@ -315,8 +315,8 @@
 <g id="node16" class="node">
 <title>red1_star</title>
 <g id="a_node16"><a xlink:title="red1_star theory/Closure.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1257" rx="31.35" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-1254.8" font-family="Inter" font-size="9.00" fill="#222222">red1_star</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1219" rx="31.35" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-1216.8" font-family="Inter" font-size="9.00" fill="#222222">red1_star</text>
 </a>
 </g>
 </g>
@@ -324,32 +324,32 @@
 <g id="node17" class="node">
 <title>Plus_to_Star</title>
 <g id="a_node17"><a xlink:title="Plus_to_Star theory/Closure.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="577.6" cy="-307" rx="39.02" ry="18"/>
-<text text-anchor="middle" x="577.6" y="-304.8" font-family="Inter" font-size="9.00" fill="#222222">Plus_to_Star</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="578.76" cy="-249" rx="39.02" ry="18"/>
+<text text-anchor="middle" x="578.76" y="-246.8" font-family="Inter" font-size="9.00" fill="#222222">Plus_to_Star</text>
 </a>
 </g>
 </g>
 <!-- star_red_sub_full_comp -->
-<g id="node123" class="node">
+<g id="node128" class="node">
 <title>star_red_sub_full_comp</title>
-<g id="a_node123"><a xlink:title="star_red_sub_full_comp theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="752.81" cy="-281" rx="65.64" ry="18"/>
-<text text-anchor="middle" x="752.81" y="-278.8" font-family="Inter" font-size="9.00" fill="#222222">star_red_sub_full_comp</text>
+<g id="a_node128"><a xlink:title="star_red_sub_full_comp theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="755.12" cy="-223" rx="65.64" ry="18"/>
+<text text-anchor="middle" x="755.12" y="-220.8" font-family="Inter" font-size="9.00" fill="#222222">star_red_sub_full_comp</text>
 </a>
 </g>
 </g>
 <!-- Plus_to_Star&#45;&gt;star_red_sub_full_comp -->
-<g id="edge83" class="edge">
+<g id="edge85" class="edge">
 <title>Plus_to_Star&#45;&gt;star_red_sub_full_comp</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M615.34,-301.49C636.57,-298.3 663.88,-294.2 688.49,-290.51"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="689.06,-292.54 694.68,-289.58 688.43,-288.39 689.06,-292.54"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M616.31,-243.55C637.94,-240.32 665.94,-236.15 691.05,-232.41"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="691.4,-234.48 697.02,-231.51 690.78,-230.32 691.4,-234.48"/>
 </g>
 <!-- Star_red1_context -->
 <g id="node18" class="node">
 <title>Star_red1_context</title>
 <g id="a_node18"><a xlink:title="Star_red1_context theory/Closure.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1309" rx="53.23" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-1306.8" font-family="Inter" font-size="9.00" fill="#222222">Star_red1_context</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1271" rx="53.23" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-1268.8" font-family="Inter" font-size="9.00" fill="#222222">Star_red1_context</text>
 </a>
 </g>
 </g>
@@ -357,8 +357,8 @@
 <g id="node19" class="node">
 <title>star_one_trans</title>
 <g id="a_node19"><a xlink:title="star_one_trans theory/Closure.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1361" rx="45.07" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-1358.8" font-family="Inter" font-size="9.00" fill="#222222">star_one_trans</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1323" rx="45.07" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-1320.8" font-family="Inter" font-size="9.00" fill="#222222">star_one_trans</text>
 </a>
 </g>
 </g>
@@ -366,8 +366,8 @@
 <g id="node20" class="node">
 <title>in_comb</title>
 <g id="a_node20"><a xlink:title="in_comb theory/Enumerate.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1465" rx="30.04" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-1462.8" font-family="Inter" font-size="9.00" fill="#222222">in_comb</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1427" rx="30.04" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-1424.8" font-family="Inter" font-size="9.00" fill="#222222">in_comb</text>
 </a>
 </g>
 </g>
@@ -375,38 +375,38 @@
 <g id="node22" class="node">
 <title>size_all_terms</title>
 <g id="a_node22"><a xlink:title="size_all_terms theory/Enumerate.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-1439" rx="43.1" ry="18"/>
-<text text-anchor="middle" x="239.88" y="-1436.8" font-family="Inter" font-size="9.00" fill="#222222">size_all_terms</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-1401" rx="43.1" ry="18"/>
+<text text-anchor="middle" x="239.88" y="-1398.8" font-family="Inter" font-size="9.00" fill="#222222">size_all_terms</text>
 </a>
 </g>
 </g>
 <!-- in_comb&#45;&gt;size_all_terms -->
 <g id="edge9" class="edge">
 <title>in_comb&#45;&gt;size_all_terms</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M94.75,-1460.71C121.41,-1456.69 161.7,-1450.62 192.91,-1445.92"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="193.4,-1447.97 199.02,-1445 192.78,-1443.82 193.4,-1447.97"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M94.75,-1422.71C121.41,-1418.69 161.7,-1412.62 192.91,-1407.92"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="193.4,-1409.97 199.02,-1407 192.78,-1405.82 193.4,-1409.97"/>
 </g>
 <!-- pow2_pos -->
 <g id="node21" class="node">
 <title>pow2_pos</title>
 <g id="a_node21"><a xlink:title="pow2_pos theory/Enumerate.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1413" rx="34.13" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-1410.8" font-family="Inter" font-size="9.00" fill="#222222">pow2_pos</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1375" rx="34.13" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-1372.8" font-family="Inter" font-size="9.00" fill="#222222">pow2_pos</text>
 </a>
 </g>
 </g>
 <!-- pow2_pos&#45;&gt;size_all_terms -->
 <g id="edge10" class="edge">
 <title>pow2_pos&#45;&gt;size_all_terms</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M98.31,-1417.83C124.8,-1421.82 162.75,-1427.54 192.55,-1432.02"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="192.53,-1434.14 198.78,-1432.96 193.16,-1429.99 192.53,-1434.14"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M98.31,-1379.83C124.8,-1383.82 162.75,-1389.54 192.55,-1394.02"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="192.53,-1396.14 198.78,-1394.96 193.16,-1391.99 192.53,-1396.14"/>
 </g>
 <!-- enumerate_check -->
 <g id="node23" class="node">
 <title>enumerate_check</title>
 <g id="a_node23"><a xlink:title="enumerate_check theory/Enumerate.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="1232.27" cy="-741" rx="53.89" ry="18"/>
-<text text-anchor="middle" x="1232.27" y="-738.8" font-family="Inter" font-size="9.00" fill="#222222">enumerate_check</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="1234.58" cy="-604" rx="53.89" ry="18"/>
+<text text-anchor="middle" x="1234.58" y="-601.8" font-family="Inter" font-size="9.00" fill="#222222">enumerate_check</text>
 </a>
 </g>
 </g>
@@ -414,8 +414,8 @@
 <g id="node24" class="node">
 <title>enumerate_sound</title>
 <g id="a_node24"><a xlink:title="enumerate_sound theory/Enumerate.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="752.81" cy="-711" rx="53.23" ry="18"/>
-<text text-anchor="middle" x="752.81" y="-708.8" font-family="Inter" font-size="9.00" fill="#222222">enumerate_sound</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="755.12" cy="-509" rx="53.23" ry="18"/>
+<text text-anchor="middle" x="755.12" y="-506.8" font-family="Inter" font-size="9.00" fill="#222222">enumerate_sound</text>
 </a>
 </g>
 </g>
@@ -423,8 +423,8 @@
 <g id="node25" class="node">
 <title>enumerate_complete</title>
 <g id="a_node25"><a xlink:title="enumerate_complete theory/Enumerate.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="752.81" cy="-521" rx="61.55" ry="18"/>
-<text text-anchor="middle" x="752.81" y="-518.8" font-family="Inter" font-size="9.00" fill="#222222">enumerate_complete</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="755.12" cy="-803" rx="61.55" ry="18"/>
+<text text-anchor="middle" x="755.12" y="-800.8" font-family="Inter" font-size="9.00" fill="#222222">enumerate_complete</text>
 </a>
 </g>
 </g>
@@ -432,8 +432,8 @@
 <g id="node26" class="node">
 <title>of_trm_fvs</title>
 <g id="a_node26"><a xlink:title="of_trm_fvs theory/Metaterm.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1517" rx="34.78" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-1514.8" font-family="Inter" font-size="9.00" fill="#222222">of_trm_fvs</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1479" rx="34.78" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-1476.8" font-family="Inter" font-size="9.00" fill="#222222">of_trm_fvs</text>
 </a>
 </g>
 </g>
@@ -441,8 +441,8 @@
 <g id="node27" class="node">
 <title>of_trm_lift</title>
 <g id="a_node27"><a xlink:title="of_trm_lift theory/Metaterm.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1569" rx="34.13" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-1566.8" font-family="Inter" font-size="9.00" fill="#222222">of_trm_lift</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1531" rx="34.13" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-1528.8" font-family="Inter" font-size="9.00" fill="#222222">of_trm_lift</text>
 </a>
 </g>
 </g>
@@ -450,23 +450,23 @@
 <g id="node28" class="node">
 <title>of_trm_open</title>
 <g id="a_node28"><a xlink:title="of_trm_open theory/Metaterm.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-1569" rx="39.02" ry="18"/>
-<text text-anchor="middle" x="239.88" y="-1566.8" font-family="Inter" font-size="9.00" fill="#222222">of_trm_open</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-1531" rx="39.02" ry="18"/>
+<text text-anchor="middle" x="239.88" y="-1528.8" font-family="Inter" font-size="9.00" fill="#222222">of_trm_open</text>
 </a>
 </g>
 </g>
 <!-- of_trm_lift&#45;&gt;of_trm_open -->
 <g id="edge14" class="edge">
 <title>of_trm_lift&#45;&gt;of_trm_open</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M99.53,-1569C126.51,-1569 164.79,-1569 194.4,-1569"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="194.58,-1571.1 200.58,-1569 194.58,-1566.9 194.58,-1571.1"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M99.53,-1531C126.51,-1531 164.79,-1531 194.4,-1531"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="194.58,-1533.1 200.58,-1531 194.58,-1528.9 194.58,-1533.1"/>
 </g>
 <!-- of_trm_close -->
 <g id="node29" class="node">
 <title>of_trm_close</title>
 <g id="a_node29"><a xlink:title="of_trm_close theory/Metaterm.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1621" rx="40.33" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-1618.8" font-family="Inter" font-size="9.00" fill="#222222">of_trm_close</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1583" rx="40.33" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-1580.8" font-family="Inter" font-size="9.00" fill="#222222">of_trm_close</text>
 </a>
 </g>
 </g>
@@ -474,8 +474,8 @@
 <g id="node30" class="node">
 <title>of_trm_injective</title>
 <g id="a_node30"><a xlink:title="of_trm_injective theory/Metaterm.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1673" rx="48.49" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-1670.8" font-family="Inter" font-size="9.00" fill="#222222">of_trm_injective</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1635" rx="48.49" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-1632.8" font-family="Inter" font-size="9.00" fill="#222222">of_trm_injective</text>
 </a>
 </g>
 </g>
@@ -483,8 +483,8 @@
 <g id="node31" class="node">
 <title>mfvs_lift_m</title>
 <g id="a_node31"><a xlink:title="mfvs_lift_m theory/Metaterm.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1725" rx="37.56" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-1722.8" font-family="Inter" font-size="9.00" fill="#222222">mfvs_lift_m</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1687" rx="37.56" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-1684.8" font-family="Inter" font-size="9.00" fill="#222222">mfvs_lift_m</text>
 </a>
 </g>
 </g>
@@ -492,23 +492,23 @@
 <g id="node33" class="node">
 <title>mfvs_open_m</title>
 <g id="a_node33"><a xlink:title="mfvs_open_m theory/Metaterm.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-1725" rx="43.1" ry="18"/>
-<text text-anchor="middle" x="239.88" y="-1722.8" font-family="Inter" font-size="9.00" fill="#222222">mfvs_open_m</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-1687" rx="43.1" ry="18"/>
+<text text-anchor="middle" x="239.88" y="-1684.8" font-family="Inter" font-size="9.00" fill="#222222">mfvs_open_m</text>
 </a>
 </g>
 </g>
 <!-- mfvs_lift_m&#45;&gt;mfvs_open_m -->
 <g id="edge15" class="edge">
 <title>mfvs_lift_m&#45;&gt;mfvs_open_m</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M102.85,-1725C128.34,-1725 162.6,-1725 190.36,-1725"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="190.54,-1727.1 196.54,-1725 190.54,-1722.9 190.54,-1727.1"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M102.85,-1687C128.34,-1687 162.6,-1687 190.36,-1687"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="190.54,-1689.1 196.54,-1687 190.54,-1684.9 190.54,-1689.1"/>
 </g>
 <!-- mfvs_close_m -->
 <g id="node32" class="node">
 <title>mfvs_close_m</title>
 <g id="a_node32"><a xlink:title="mfvs_close_m theory/Metaterm.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1777" rx="44.41" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-1774.8" font-family="Inter" font-size="9.00" fill="#222222">mfvs_close_m</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1739" rx="44.41" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-1736.8" font-family="Inter" font-size="9.00" fill="#222222">mfvs_close_m</text>
 </a>
 </g>
 </g>
@@ -516,8 +516,8 @@
 <g id="node34" class="node">
 <title>of_trm_plug</title>
 <g id="a_node34"><a xlink:title="of_trm_plug theory/Metaterm.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1829" rx="38.21" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-1826.8" font-family="Inter" font-size="9.00" fill="#222222">of_trm_plug</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1791" rx="38.21" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-1788.8" font-family="Inter" font-size="9.00" fill="#222222">of_trm_plug</text>
 </a>
 </g>
 </g>
@@ -525,23 +525,23 @@
 <g id="node37" class="node">
 <title>mred_term_context</title>
 <g id="a_node37"><a xlink:title="mred_term_context theory/Metaterm.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-1829" rx="56.66" ry="18"/>
-<text text-anchor="middle" x="239.88" y="-1826.8" font-family="Inter" font-size="9.00" fill="#222222">mred_term_context</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-1791" rx="56.66" ry="18"/>
+<text text-anchor="middle" x="239.88" y="-1788.8" font-family="Inter" font-size="9.00" fill="#222222">mred_term_context</text>
 </a>
 </g>
 </g>
 <!-- of_trm_plug&#45;&gt;mred_term_context -->
 <g id="edge16" class="edge">
 <title>of_trm_plug&#45;&gt;mred_term_context</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M103.7,-1829C125.09,-1829 152.45,-1829 176.96,-1829"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="177.12,-1831.1 183.12,-1829 177.12,-1826.9 177.12,-1831.1"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M103.7,-1791C125.09,-1791 152.45,-1791 176.96,-1791"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="177.12,-1793.1 183.12,-1791 177.12,-1788.9 177.12,-1793.1"/>
 </g>
 <!-- mred_of_red1 -->
 <g id="node35" class="node">
 <title>mred_of_red1</title>
 <g id="a_node35"><a xlink:title="mred_of_red1 theory/Metaterm.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1881" rx="41.64" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-1878.8" font-family="Inter" font-size="9.00" fill="#222222">mred_of_red1</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1843" rx="41.64" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-1840.8" font-family="Inter" font-size="9.00" fill="#222222">mred_of_red1</text>
 </a>
 </g>
 </g>
@@ -549,8 +549,8 @@
 <g id="node36" class="node">
 <title>mred_context</title>
 <g id="a_node36"><a xlink:title="mred_context theory/Metaterm.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1933" rx="42.95" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-1930.8" font-family="Inter" font-size="9.00" fill="#222222">mred_context</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1895" rx="42.95" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-1892.8" font-family="Inter" font-size="9.00" fill="#222222">mred_context</text>
 </a>
 </g>
 </g>
@@ -558,8 +558,8 @@
 <g id="node38" class="node">
 <title>of_trm_moccurs</title>
 <g id="a_node38"><a xlink:title="of_trm_moccurs theory/Metaterm.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1985" rx="49.8" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-1982.8" font-family="Inter" font-size="9.00" fill="#222222">of_trm_moccurs</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1947" rx="49.8" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-1944.8" font-family="Inter" font-size="9.00" fill="#222222">of_trm_moccurs</text>
 </a>
 </g>
 </g>
@@ -567,23 +567,23 @@
 <g id="node39" class="node">
 <title>of_trm_moccurs0</title>
 <g id="a_node39"><a xlink:title="of_trm_moccurs0 theory/Metaterm.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-1985" rx="53.23" ry="18"/>
-<text text-anchor="middle" x="239.88" y="-1982.8" font-family="Inter" font-size="9.00" fill="#222222">of_trm_moccurs0</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-1947" rx="53.23" ry="18"/>
+<text text-anchor="middle" x="239.88" y="-1944.8" font-family="Inter" font-size="9.00" fill="#222222">of_trm_moccurs0</text>
 </a>
 </g>
 </g>
 <!-- of_trm_moccurs&#45;&gt;of_trm_moccurs0 -->
 <g id="edge17" class="edge">
 <title>of_trm_moccurs&#45;&gt;of_trm_moccurs0</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M115.25,-1985C135.57,-1985 159.31,-1985 180.53,-1985"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="180.73,-1987.1 186.73,-1985 180.73,-1982.9 180.73,-1987.1"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M115.25,-1947C135.57,-1947 159.31,-1947 180.53,-1947"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="180.73,-1949.1 186.73,-1947 180.73,-1944.9 180.73,-1949.1"/>
 </g>
 <!-- mred_B_intro -->
 <g id="node40" class="node">
 <title>mred_B_intro</title>
 <g id="a_node40"><a xlink:title="mred_B_intro theory/Metaterm.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-2037" rx="41.64" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-2034.8" font-family="Inter" font-size="9.00" fill="#222222">mred_B_intro</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-1999" rx="41.64" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-1996.8" font-family="Inter" font-size="9.00" fill="#222222">mred_B_intro</text>
 </a>
 </g>
 </g>
@@ -591,8 +591,8 @@
 <g id="node41" class="node">
 <title>mred_gc_intro</title>
 <g id="a_node41"><a xlink:title="mred_gc_intro theory/Metaterm.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-2089" rx="43.76" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-2086.8" font-family="Inter" font-size="9.00" fill="#222222">mred_gc_intro</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-2051" rx="43.76" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-2048.8" font-family="Inter" font-size="9.00" fill="#222222">mred_gc_intro</text>
 </a>
 </g>
 </g>
@@ -600,1153 +600,1210 @@
 <g id="node42" class="node">
 <title>mred_r_intro</title>
 <g id="a_node42"><a xlink:title="mred_r_intro theory/Metaterm.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-2141" rx="40.33" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-2138.8" font-family="Inter" font-size="9.00" fill="#222222">mred_r_intro</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-2103" rx="40.33" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-2100.8" font-family="Inter" font-size="9.00" fill="#222222">mred_r_intro</text>
+</a>
+</g>
+</g>
+<!-- Plus_mred_of_Plus_red1 -->
+<g id="node43" class="node">
+<title>Plus_mred_of_Plus_red1</title>
+<g id="a_node43"><a xlink:title="Plus_mred_of_Plus_red1 theory/Metaterm.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="578.76" cy="-405" rx="67.6" ry="18"/>
+<text text-anchor="middle" x="578.76" y="-402.8" font-family="Inter" font-size="9.00" fill="#222222">Plus_mred_of_Plus_red1</text>
+</a>
+</g>
+</g>
+<!-- mred_full_comp_pure -->
+<g id="node44" class="node">
+<title>mred_full_comp_pure</title>
+<g id="a_node44"><a xlink:title="mred_full_comp_pure theory/Metaterm.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="755.12" cy="-353" rx="61.4" ry="18"/>
+<text text-anchor="middle" x="755.12" y="-350.8" font-family="Inter" font-size="9.00" fill="#222222">mred_full_comp_pure</text>
+</a>
+</g>
+</g>
+<!-- Plus_mred_of_Plus_red1&#45;&gt;mred_full_comp_pure -->
+<g id="edge18" class="edge">
+<title>Plus_mred_of_Plus_red1&#45;&gt;mred_full_comp_pure</title>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M624.66,-391.61C649.42,-384.23 680.17,-375.05 705.49,-367.5"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="706.32,-369.45 711.47,-365.72 705.12,-365.42 706.32,-369.45"/>
+</g>
+<!-- mred_plus_one -->
+<g id="node45" class="node">
+<title>mred_plus_one</title>
+<g id="a_node45"><a xlink:title="mred_plus_one theory/Metaterm.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-2155" rx="46.38" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-2152.8" font-family="Inter" font-size="9.00" fill="#222222">mred_plus_one</text>
 </a>
 </g>
 </g>
 <!-- Plus_red1_context -->
-<g id="node43" class="node">
+<g id="node46" class="node">
 <title>Plus_red1_context</title>
-<g id="a_node43"><a xlink:title="Plus_red1_context theory/Metatheory.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="577.6" cy="-411" rx="53.23" ry="18"/>
-<text text-anchor="middle" x="577.6" y="-408.8" font-family="Inter" font-size="9.00" fill="#222222">Plus_red1_context</text>
+<g id="a_node46"><a xlink:title="Plus_red1_context theory/Metatheory.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="578.76" cy="-301" rx="53.23" ry="18"/>
+<text text-anchor="middle" x="578.76" y="-298.8" font-family="Inter" font-size="9.00" fill="#222222">Plus_red1_context</text>
 </a>
 </g>
 </g>
 <!-- lemma_2_3_beta_sim -->
-<g id="node58" class="node">
+<g id="node61" class="node">
 <title>lemma_2_3_beta_sim</title>
-<g id="a_node58"><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="M793.81,-403C793.81,-403 711.81,-403 711.81,-403 705.81,-403 699.81,-397 699.81,-391 699.81,-391 699.81,-379 699.81,-379 699.81,-373 705.81,-367 711.81,-367 711.81,-367 793.81,-367 793.81,-367 799.81,-367 805.81,-373 805.81,-379 805.81,-379 805.81,-391 805.81,-391 805.81,-397 799.81,-403 793.81,-403"/>
-<text text-anchor="middle" x="752.81" y="-382.8" font-family="Inter" font-size="9.00" fill="#222222">lemma_2_3_beta_sim</text>
+<g id="a_node61"><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="M796.12,-319C796.12,-319 714.12,-319 714.12,-319 708.12,-319 702.12,-313 702.12,-307 702.12,-307 702.12,-295 702.12,-295 702.12,-289 708.12,-283 714.12,-283 714.12,-283 796.12,-283 796.12,-283 802.12,-283 808.12,-289 808.12,-295 808.12,-295 808.12,-307 808.12,-307 808.12,-313 802.12,-319 796.12,-319"/>
+<text text-anchor="middle" x="755.12" y="-298.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="edge35" class="edge">
+<g id="edge37" class="edge">
 <title>Plus_red1_context&#45;&gt;lemma_2_3_beta_sim</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M626.39,-403.83C647.17,-400.71 671.7,-397.02 693.54,-393.75"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="694,-395.8 699.62,-392.83 693.38,-391.65 694,-395.8"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M632.07,-301C652.16,-301 675.2,-301 695.82,-301"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="695.84,-303.1 701.84,-301 695.84,-298.9 695.84,-303.1"/>
 </g>
 <!-- occurs_count_zero -->
-<g id="node44" class="node">
+<g id="node47" class="node">
 <title>occurs_count_zero</title>
-<g id="a_node44"><a xlink:title="occurs_count_zero theory/Metatheory.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-208" rx="54.7" ry="18"/>
-<text text-anchor="middle" x="239.88" y="-205.8" font-family="Inter" font-size="9.00" fill="#222222">occurs_count_zero</text>
+<g id="a_node47"><a xlink:title="occurs_count_zero theory/Metatheory.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-122" rx="54.7" ry="18"/>
+<text text-anchor="middle" x="239.88" y="-119.8" font-family="Inter" font-size="9.00" fill="#222222">occurs_count_zero</text>
 </a>
 </g>
 </g>
 <!-- occurs_count_pos -->
-<g id="node46" class="node">
+<g id="node49" class="node">
 <title>occurs_count_pos</title>
-<g id="a_node46"><a xlink:title="occurs_count_pos theory/Metatheory.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-205" rx="53.89" ry="18"/>
-<text text-anchor="middle" x="408.74" y="-202.8" font-family="Inter" font-size="9.00" fill="#222222">occurs_count_pos</text>
+<g id="a_node49"><a xlink:title="occurs_count_pos theory/Metatheory.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-122" rx="53.89" ry="18"/>
+<text text-anchor="middle" x="408.74" y="-119.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="edge18" class="edge">
+<g id="edge20" class="edge">
 <title>occurs_count_zero&#45;&gt;occurs_count_pos</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M295.05,-207.03C312.17,-206.72 331.17,-206.38 348.62,-206.06"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="349.01,-208.16 354.97,-205.95 348.94,-203.96 349.01,-208.16"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M295.05,-122C312.17,-122 331.17,-122 348.62,-122"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="348.97,-124.1 354.97,-122 348.97,-119.9 348.97,-124.1"/>
 </g>
 <!-- occurs_count_zero&#45;&gt;full_comp_aux -->
-<g id="edge23" class="edge">
+<g id="edge25" class="edge">
 <title>occurs_count_zero&#45;&gt;full_comp_aux</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M280.55,-220.13C289.46,-223.82 298.55,-228.42 306.27,-234 311.41,-237.71 362.06,-299.19 389.8,-333.05"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="388.29,-334.52 393.72,-337.83 391.54,-331.86 388.29,-334.52"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M283.12,-133.27C291.51,-136.95 299.73,-141.76 306.27,-148 339.8,-180 328.83,-201.41 349.27,-243 364.22,-273.42 382.78,-307.82 394.92,-329.92"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="393.13,-331.03 397.87,-335.27 396.81,-329 393.13,-331.03"/>
 </g>
 <!-- occurs_count_zero&#45;&gt;full_comp_aux_sub -->
-<g id="edge74" class="edge">
+<g id="edge76" class="edge">
 <title>occurs_count_zero&#45;&gt;full_comp_aux_sub</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M281.27,-219.86C305.38,-226.94 336.09,-235.96 361.21,-243.34"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="360.79,-245.4 367.14,-245.08 361.97,-241.37 360.79,-245.4"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M277.83,-135.06C287.29,-138.84 297.31,-143.25 306.27,-148 333.16,-162.27 361.65,-182.1 381.57,-196.85"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="380.37,-198.58 386.44,-200.48 382.88,-195.21 380.37,-198.58"/>
 </g>
 <!-- occurs_count_false -->
-<g id="node45" class="node">
+<g id="node48" class="node">
 <title>occurs_count_false</title>
-<g id="a_node45"><a xlink:title="occurs_count_false theory/Metatheory.v https://arxiv.org/html/2312.13270v1">
+<g id="a_node48"><a xlink:title="occurs_count_false theory/Metatheory.v https://arxiv.org/html/2312.13270v1">
 <ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-398" rx="56.66" ry="18"/>
 <text text-anchor="middle" x="65.24" y="-395.8" font-family="Inter" font-size="9.00" fill="#222222">occurs_count_false</text>
 </a>
 </g>
 </g>
 <!-- occurs_count_zfill_plug -->
-<g id="node49" class="node">
+<g id="node52" class="node">
 <title>occurs_count_zfill_plug</title>
-<g id="a_node49"><a xlink:title="occurs_count_zfill_plug theory/Metatheory.v https://arxiv.org/html/2312.13270v1">
+<g id="a_node52"><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="-398" rx="66.29" ry="18"/>
 <text text-anchor="middle" x="239.88" y="-395.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="edge19" class="edge">
+<g id="edge21" 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,-398C136.5,-398 151.97,-398 166.86,-398"/>
 <polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="167.2,-400.1 173.2,-398 167.2,-395.9 167.2,-400.1"/>
 </g>
 <!-- occurs_lift_self -->
-<g id="node47" class="node">
+<g id="node50" class="node">
 <title>occurs_lift_self</title>
-<g id="a_node47"><a xlink:title="occurs_lift_self theory/Metatheory.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-329" rx="46.38" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-326.8" font-family="Inter" font-size="9.00" fill="#222222">occurs_lift_self</text>
+<g id="a_node50"><a xlink:title="occurs_lift_self theory/Metatheory.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-318" rx="46.38" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-315.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="edge20" class="edge">
+<g id="edge22" class="edge">
 <title>occurs_lift_self&#45;&gt;occurs_count_zfill_plug</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M98.31,-341.82C125.82,-352.81 165.71,-368.76 195.97,-380.85"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="195.54,-382.94 201.89,-383.22 197.1,-379.04 195.54,-382.94"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M95.8,-331.84C117.33,-341.91 147.19,-355.84 173.48,-368 181.86,-371.88 190.86,-376.02 199.41,-379.94"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="198.92,-382.03 205.25,-382.62 200.68,-378.21 198.92,-382.03"/>
 </g>
 <!-- occurs_lift_self&#45;&gt;open_rec_zplug_lift -->
-<g id="edge21" class="edge">
+<g id="edge23" class="edge">
 <title>occurs_lift_self&#45;&gt;open_rec_zplug_lift</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M98.14,-316.18C119.46,-307.62 148.15,-296.12 173.48,-286 181.26,-282.9 189.56,-279.59 197.54,-276.41"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="198.77,-278.18 203.57,-274.01 197.22,-274.28 198.77,-278.18"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M100.76,-306.4C127.7,-297.35 165.31,-284.71 194.49,-274.91"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="195.19,-276.89 200.2,-272.99 193.85,-272.91 195.19,-276.89"/>
 </g>
 <!-- zdecs_nonempty -->
-<g id="node48" class="node">
+<g id="node51" class="node">
 <title>zdecs_nonempty</title>
-<g id="a_node48"><a xlink:title="zdecs_nonempty theory/Metatheory.v https://arxiv.org/html/2312.13270v1">
+<g id="a_node51"><a xlink:title="zdecs_nonempty theory/Metatheory.v https://arxiv.org/html/2312.13270v1">
 <ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-312" rx="51.27" ry="18"/>
 <text text-anchor="middle" x="239.88" y="-309.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="edge27" class="edge">
+<g id="edge29" class="edge">
 <title>zdecs_nonempty&#45;&gt;full_comp_aux</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M281.7,-322.52C306.88,-329.01 339.16,-337.33 364.74,-343.92"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="364.42,-346.01 370.76,-345.47 365.47,-341.94 364.42,-346.01"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M282.55,-322.24C307.49,-328.37 339.12,-336.14 364.35,-342.34"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="363.96,-344.41 370.29,-343.8 364.97,-340.33 363.96,-344.41"/>
 </g>
 <!-- zdecs_nonempty&#45;&gt;full_comp_aux_sub -->
-<g id="edge80" class="edge">
+<g id="edge82" class="edge">
 <title>zdecs_nonempty&#45;&gt;full_comp_aux_sub</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M277.91,-299.79C303.17,-291.47 336.75,-280.4 363.43,-271.6"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="364.32,-273.52 369.36,-269.65 363.01,-269.53 364.32,-273.52"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M276.81,-299.35C286.56,-295.47 296.99,-290.92 306.27,-286 333.16,-271.73 361.65,-251.9 381.57,-237.15"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="382.88,-238.79 386.44,-233.52 380.37,-235.42 382.88,-238.79"/>
 </g>
 <!-- occurs_count_zfill_plug&#45;&gt;full_comp_aux -->
-<g id="edge24" class="edge">
+<g id="edge26" class="edge">
 <title>occurs_count_zfill_plug&#45;&gt;full_comp_aux</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M288.69,-385.68C312.65,-379.5 341.43,-372.09 364.69,-366.09"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="365.5,-368.05 370.79,-364.52 364.45,-363.99 365.5,-368.05"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M287.8,-385.35C312.15,-378.78 341.67,-370.82 365.32,-364.44"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="365.96,-366.44 371.21,-362.85 364.87,-362.39 365.96,-366.44"/>
 </g>
 <!-- occurs_count_zfill_plug&#45;&gt;full_comp_aux_sub -->
-<g id="edge75" class="edge">
+<g id="edge77" class="edge">
 <title>occurs_count_zfill_plug&#45;&gt;full_comp_aux_sub</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M261.34,-380.71C292.11,-354.71 350.21,-305.61 383.21,-277.73"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="384.66,-279.25 387.89,-273.77 381.95,-276.04 384.66,-279.25"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M260.97,-380.79C274.24,-369.13 291.79,-353.14 306.27,-338 337.71,-305.12 371.03,-264.03 390.57,-239.18"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="392.25,-240.46 394.3,-234.44 388.94,-237.86 392.25,-240.46"/>
 </g>
 <!-- open_rec_zplug_lift&#45;&gt;full_comp_aux -->
-<g id="edge26" class="edge">
+<g id="edge28" class="edge">
 <title>open_rec_zplug_lift&#45;&gt;full_comp_aux</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M278.52,-273.34C287.77,-277.06 297.53,-281.36 306.27,-286 333.51,-300.45 362.38,-320.62 382.33,-335.42"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="381.14,-337.15 387.21,-339.06 383.66,-333.78 381.14,-337.15"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M278.13,-273.28C287.49,-277.03 297.39,-281.36 306.27,-286 333.19,-300.05 361.88,-319.45 381.86,-333.77"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="380.66,-335.49 386.75,-337.29 383.11,-332.08 380.66,-335.49"/>
 </g>
 <!-- open_rec_zplug_lift&#45;&gt;full_comp_aux_sub -->
-<g id="edge77" class="edge">
+<g id="edge79" class="edge">
 <title>open_rec_zplug_lift&#45;&gt;full_comp_aux_sub</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M296.44,-259C312.9,-258.71 331.01,-258.38 347.74,-258.08"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="347.87,-260.18 353.84,-257.97 347.8,-255.98 347.87,-260.18"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M284.28,-248.81C307.25,-242.9 335.52,-235.61 359.21,-229.51"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="359.84,-231.51 365.13,-227.98 358.79,-227.44 359.84,-231.51"/>
 </g>
 <!-- lemma_2_2_full_comp -->
-<g id="node52" class="node">
+<g id="node55" class="node">
 <title>lemma_2_2_full_comp</title>
-<g id="a_node52"><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="M619.6,-377C619.6,-377 535.6,-377 535.6,-377 529.6,-377 523.6,-371 523.6,-365 523.6,-365 523.6,-353 523.6,-353 523.6,-347 529.6,-341 535.6,-341 535.6,-341 619.6,-341 619.6,-341 625.6,-341 631.6,-347 631.6,-353 631.6,-353 631.6,-365 631.6,-365 631.6,-371 625.6,-377 619.6,-377"/>
-<text text-anchor="middle" x="577.6" y="-356.8" font-family="Inter" font-size="9.00" fill="#222222">lemma_2_2_full_comp</text>
+<g id="a_node55"><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="M620.76,-371C620.76,-371 536.76,-371 536.76,-371 530.76,-371 524.76,-365 524.76,-359 524.76,-359 524.76,-347 524.76,-347 524.76,-341 530.76,-335 536.76,-335 536.76,-335 620.76,-335 620.76,-335 626.76,-335 632.76,-341 632.76,-347 632.76,-347 632.76,-359 632.76,-359 632.76,-365 626.76,-371 620.76,-371"/>
+<text text-anchor="middle" x="578.76" y="-350.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="edge29" class="edge">
+<g id="edge31" 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.14,-356.04C472.74,-356.51 496.2,-357.07 517.39,-357.58"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="517.54,-359.68 523.59,-357.73 517.64,-355.49 517.54,-359.68"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M453.44,-353C473.27,-353 497.01,-353 518.42,-353"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="518.68,-355.1 524.68,-353 518.68,-350.9 518.68,-355.1"/>
+</g>
+<!-- lemma_2_2_full_comp&#45;&gt;mred_full_comp_pure -->
+<g id="edge19" class="edge">
+<title>lemma_2_2_full_comp&#45;&gt;mred_full_comp_pure</title>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M633.02,-353C650.3,-353 669.68,-353 687.79,-353"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="687.87,-355.1 693.87,-353 687.87,-350.9 687.87,-355.1"/>
 </g>
 <!-- lemma_2_2_full_comp&#45;&gt;lemma_2_3_beta_sim -->
-<g id="edge36" class="edge">
+<g id="edge38" 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="M631.98,-367.01C651.53,-369.95 673.74,-373.28 693.69,-376.27"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="693.55,-378.38 699.8,-377.19 694.17,-374.22 693.55,-378.38"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M633.02,-337.12C652.98,-331.16 675.76,-324.37 696.13,-318.3"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="696.93,-320.25 702.08,-316.52 695.73,-316.22 696.93,-320.25"/>
 </g>
 <!-- red1_root_fv -->
-<g id="node55" class="node">
+<g id="node58" class="node">
 <title>red1_root_fv</title>
-<g id="a_node55"><a xlink:title="red1_root_fv theory/Metatheory.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-893" rx="38.87" ry="18"/>
-<text text-anchor="middle" x="408.74" y="-890.8" font-family="Inter" font-size="9.00" fill="#222222">red1_root_fv</text>
+<g id="a_node58"><a xlink:title="red1_root_fv theory/Metatheory.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-855" rx="38.87" ry="18"/>
+<text text-anchor="middle" x="408.74" y="-852.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="edge31" class="edge">
+<g id="edge33" class="edge">
 <title>fvs_zplug_lift&#45;&gt;red1_root_fv</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M281.27,-893C306.27,-893 338.37,-893 363.98,-893"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="364.01,-895.1 370.01,-893 364.01,-890.9 364.01,-895.1"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M281.27,-855C306.27,-855 338.37,-855 363.98,-855"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="364.01,-857.1 370.01,-855 364.01,-852.9 364.01,-857.1"/>
 </g>
 <!-- plug_fv_mono -->
-<g id="node54" class="node">
+<g id="node57" class="node">
 <title>plug_fv_mono</title>
-<g id="a_node54"><a xlink:title="plug_fv_mono theory/Metatheory.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-945" rx="42.95" ry="18"/>
-<text text-anchor="middle" x="408.74" y="-942.8" font-family="Inter" font-size="9.00" fill="#222222">plug_fv_mono</text>
+<g id="a_node57"><a xlink:title="plug_fv_mono theory/Metatheory.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-907" rx="42.95" ry="18"/>
+<text text-anchor="middle" x="408.74" y="-904.8" font-family="Inter" font-size="9.00" fill="#222222">plug_fv_mono</text>
 </a>
 </g>
 </g>
 <!-- red1r_fv -->
-<g id="node56" class="node">
+<g id="node59" class="node">
 <title>red1r_fv</title>
-<g id="a_node56"><a xlink:title="red1r_fv theory/Metatheory.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="577.6" cy="-919" rx="28.74" ry="18"/>
-<text text-anchor="middle" x="577.6" y="-916.8" font-family="Inter" font-size="9.00" fill="#222222">red1r_fv</text>
+<g id="a_node59"><a xlink:title="red1r_fv theory/Metatheory.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="578.76" cy="-855" rx="28.74" ry="18"/>
+<text text-anchor="middle" x="578.76" y="-852.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="edge32" class="edge">
+<g id="edge34" class="edge">
 <title>plug_fv_mono&#45;&gt;red1r_fv</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M449.28,-938.84C477.95,-934.37 516.29,-928.4 543.38,-924.18"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="543.72,-926.25 549.33,-923.25 543.08,-922.1 543.72,-926.25"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M443.74,-896.48C473.82,-887.17 517.35,-873.7 546.55,-864.66"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="547.45,-866.58 552.56,-862.8 546.2,-862.57 547.45,-866.58"/>
 </g>
 <!-- red1_root_fv&#45;&gt;red1r_fv -->
-<g id="edge33" class="edge">
+<g id="edge35" class="edge">
 <title>red1_root_fv&#45;&gt;red1r_fv</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M445.53,-898.58C474.47,-903.09 514.9,-909.39 543.18,-913.79"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="543.12,-915.91 549.38,-914.76 543.77,-911.76 543.12,-915.91"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M447.45,-855C476.32,-855 515.8,-855 543.72,-855"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="543.85,-857.1 549.85,-855 543.85,-852.9 543.85,-857.1"/>
 </g>
 <!-- lemma_2_1_fv_preserved -->
-<g id="node57" class="node">
+<g id="node60" class="node">
 <title>lemma_2_1_fv_preserved</title>
-<g id="a_node57"><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="M800.81,-937C800.81,-937 704.81,-937 704.81,-937 698.81,-937 692.81,-931 692.81,-925 692.81,-925 692.81,-913 692.81,-913 692.81,-907 698.81,-901 704.81,-901 704.81,-901 800.81,-901 800.81,-901 806.81,-901 812.81,-907 812.81,-913 812.81,-913 812.81,-925 812.81,-925 812.81,-931 806.81,-937 800.81,-937"/>
-<text text-anchor="middle" x="752.81" y="-916.8" font-family="Inter" font-size="9.00" fill="#222222">lemma_2_1_fv_preserved</text>
+<g id="a_node60"><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="M803.12,-873C803.12,-873 707.12,-873 707.12,-873 701.12,-873 695.12,-867 695.12,-861 695.12,-861 695.12,-849 695.12,-849 695.12,-843 701.12,-837 707.12,-837 707.12,-837 803.12,-837 803.12,-837 809.12,-837 815.12,-843 815.12,-849 815.12,-849 815.12,-861 815.12,-861 815.12,-867 809.12,-873 803.12,-873"/>
+<text text-anchor="middle" x="755.12" y="-852.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="edge34" class="edge">
+<g id="edge36" class="edge">
 <title>red1r_fv&#45;&gt;lemma_2_1_fv_preserved</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M606.82,-919C628.38,-919 659,-919 686.54,-919"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="686.73,-921.1 692.73,-919 686.73,-916.9 686.73,-921.1"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M607.77,-855C629.61,-855 660.82,-855 688.82,-855"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="689.11,-857.1 695.11,-855 689.11,-852.9 689.11,-857.1"/>
 </g>
 <!-- gen_fv_preserved -->
-<g id="node78" class="node">
+<g id="node83" class="node">
 <title>gen_fv_preserved</title>
-<g id="a_node78"><a xlink:title="gen_fv_preserved theory/Random.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="921.68" cy="-830" rx="52.58" ry="18"/>
-<text text-anchor="middle" x="921.68" y="-827.8" font-family="Inter" font-size="9.00" fill="#222222">gen_fv_preserved</text>
+<g id="a_node83"><a xlink:title="gen_fv_preserved theory/Random.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="923.99" cy="-755" rx="52.58" ry="18"/>
+<text text-anchor="middle" x="923.99" y="-752.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="edge44" class="edge">
+<g id="edge46" class="edge">
 <title>lemma_2_1_fv_preserved&#45;&gt;gen_fv_preserved</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M801.67,-900.89C807.45,-898.39 813.22,-895.73 818.63,-893 844.23,-880.09 871.81,-862.84 891.84,-849.65"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="893.18,-851.29 897.02,-846.22 890.86,-847.78 893.18,-851.29"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M804.87,-836.97C810.38,-834.48 815.85,-831.81 820.94,-829 849.02,-813.5 878.4,-791.49 898.39,-775.5"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="899.9,-776.98 903.26,-771.58 897.27,-773.71 899.9,-776.98"/>
 </g>
 <!-- corpus_fv_preserved -->
-<g id="node131" class="node">
+<g id="node136" class="node">
 <title>corpus_fv_preserved</title>
-<g id="a_node131"><a xlink:title="corpus_fv_preserved theory/Tests.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="921.68" cy="-900" rx="60.09" ry="18"/>
-<text text-anchor="middle" x="921.68" y="-897.8" font-family="Inter" font-size="9.00" fill="#222222">corpus_fv_preserved</text>
+<g id="a_node136"><a xlink:title="corpus_fv_preserved theory/Tests.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="923.99" cy="-831" rx="60.09" ry="18"/>
+<text text-anchor="middle" x="923.99" y="-828.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="edge91" class="edge">
+<g id="edge93" class="edge">
 <title>lemma_2_1_fv_preserved&#45;&gt;corpus_fv_preserved</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M813.11,-912.25C827.95,-910.56 843.9,-908.74 858.85,-907.04"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="859.47,-909.08 865.2,-906.32 859,-904.91 859.47,-909.08"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M815.42,-846.47C830.97,-844.23 847.74,-841.82 863.31,-839.58"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="863.8,-841.63 869.44,-838.7 863.2,-837.48 863.8,-841.63"/>
 </g>
 <!-- Plus_trans -->
-<g id="node59" class="node">
+<g id="node62" class="node">
 <title>Plus_trans</title>
-<g id="a_node59"><a xlink:title="Plus_trans theory/Metatheory.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-2193" rx="34.78" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-2190.8" font-family="Inter" font-size="9.00" fill="#222222">Plus_trans</text>
+<g id="a_node62"><a xlink:title="Plus_trans theory/Metatheory.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-2207" rx="34.78" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-2204.8" font-family="Inter" font-size="9.00" fill="#222222">Plus_trans</text>
 </a>
 </g>
 </g>
 <!-- Plus_step_trans -->
-<g id="node60" class="node">
+<g id="node63" class="node">
 <title>Plus_step_trans</title>
-<g id="a_node60"><a xlink:title="Plus_step_trans theory/Metatheory.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-2245" rx="47.19" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-2242.8" font-family="Inter" font-size="9.00" fill="#222222">Plus_step_trans</text>
+<g id="a_node63"><a xlink:title="Plus_step_trans theory/Metatheory.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-2259" rx="47.19" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-2256.8" font-family="Inter" font-size="9.00" fill="#222222">Plus_step_trans</text>
 </a>
 </g>
 </g>
 <!-- isubst_meta_in -->
-<g id="node61" class="node">
+<g id="node64" class="node">
 <title>isubst_meta_in</title>
-<g id="a_node61"><a xlink:title="isubst_meta_in theory/NamedMeta.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-2297" rx="46.38" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-2294.8" font-family="Inter" font-size="9.00" fill="#222222">isubst_meta_in</text>
+<g id="a_node64"><a xlink:title="isubst_meta_in theory/NamedMeta.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-2311" rx="46.38" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-2308.8" font-family="Inter" font-size="9.00" fill="#222222">isubst_meta_in</text>
 </a>
 </g>
 </g>
 <!-- isubst_meta_notin -->
-<g id="node62" class="node">
+<g id="node65" class="node">
 <title>isubst_meta_notin</title>
-<g id="a_node62"><a xlink:title="isubst_meta_notin theory/NamedMeta.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-2349" rx="53.89" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-2346.8" font-family="Inter" font-size="9.00" fill="#222222">isubst_meta_notin</text>
+<g id="a_node65"><a xlink:title="isubst_meta_notin theory/NamedMeta.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-2363" rx="53.89" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-2360.8" font-family="Inter" font-size="9.00" fill="#222222">isubst_meta_notin</text>
 </a>
 </g>
 </g>
 <!-- eqC_in_Es -->
-<g id="node63" class="node">
+<g id="node66" class="node">
 <title>eqC_in_Es</title>
-<g id="a_node63"><a xlink:title="eqC_in_Es theory/NamedMeta.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-2401" rx="34.13" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-2398.8" font-family="Inter" font-size="9.00" fill="#222222">eqC_in_Es</text>
+<g id="a_node66"><a xlink:title="eqC_in_Es theory/NamedMeta.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-2415" rx="34.13" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-2412.8" font-family="Inter" font-size="9.00" fill="#222222">eqC_in_Es</text>
+</a>
+</g>
+</g>
+<!-- Es_ctx_any -->
+<g id="node67" class="node">
+<title>Es_ctx_any</title>
+<g id="a_node67"><a xlink:title="Es_ctx_any theory/NamedMeta.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-2467" rx="36.25" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-2464.8" font-family="Inter" font-size="9.00" fill="#222222">Es_ctx_any</text>
+</a>
+</g>
+</g>
+<!-- nred_R_intro -->
+<g id="node68" class="node">
+<title>nred_R_intro</title>
+<g id="a_node68"><a xlink:title="nred_R_intro theory/NamedMeta.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-2519" rx="39.67" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-2516.8" font-family="Inter" font-size="9.00" fill="#222222">nred_R_intro</text>
 </a>
 </g>
 </g>
 <!-- Es_refl_any -->
-<g id="node64" class="node">
+<g id="node69" class="node">
 <title>Es_refl_any</title>
-<g id="a_node64"><a xlink:title="Es_refl_any theory/NamedMeta.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-2453" rx="36.9" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-2450.8" font-family="Inter" font-size="9.00" fill="#222222">Es_refl_any</text>
+<g id="a_node69"><a xlink:title="Es_refl_any theory/NamedMeta.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-2571" rx="36.9" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-2568.8" font-family="Inter" font-size="9.00" fill="#222222">Es_refl_any</text>
 </a>
 </g>
 </g>
 <!-- Es_sym_any -->
-<g id="node65" class="node">
+<g id="node70" class="node">
 <title>Es_sym_any</title>
-<g id="a_node65"><a xlink:title="Es_sym_any theory/NamedMeta.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-2505" rx="39.02" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-2502.8" font-family="Inter" font-size="9.00" fill="#222222">Es_sym_any</text>
+<g id="a_node70"><a xlink:title="Es_sym_any theory/NamedMeta.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-2623" rx="39.02" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-2620.8" font-family="Inter" font-size="9.00" fill="#222222">Es_sym_any</text>
 </a>
 </g>
 </g>
 <!-- Es_trans_any -->
-<g id="node66" class="node">
+<g id="node71" class="node">
 <title>Es_trans_any</title>
-<g id="a_node66"><a xlink:title="Es_trans_any theory/NamedMeta.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-2557" rx="40.98" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-2554.8" font-family="Inter" font-size="9.00" fill="#222222">Es_trans_any</text>
+<g id="a_node71"><a xlink:title="Es_trans_any theory/NamedMeta.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-2675" rx="40.98" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-2672.8" font-family="Inter" font-size="9.00" fill="#222222">Es_trans_any</text>
 </a>
 </g>
 </g>
 <!-- par_red1_iff -->
-<g id="node67" class="node">
+<g id="node72" class="node">
 <title>par_red1_iff</title>
-<g id="a_node67"><a xlink:title="par_red1_iff theory/Parallel.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-2609" rx="37.56" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-2606.8" font-family="Inter" font-size="9.00" fill="#222222">par_red1_iff</text>
+<g id="a_node72"><a xlink:title="par_red1_iff theory/Parallel.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-2727" rx="37.56" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-2724.8" font-family="Inter" font-size="9.00" fill="#222222">par_red1_iff</text>
 </a>
 </g>
 </g>
 <!-- par_to_red1_or_eq -->
-<g id="node70" class="node">
+<g id="node75" class="node">
 <title>par_to_red1_or_eq</title>
-<g id="a_node70"><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="-2635" rx="53.23" ry="18"/>
-<text text-anchor="middle" x="239.88" y="-2632.8" font-family="Inter" font-size="9.00" fill="#222222">par_to_red1_or_eq</text>
+<g id="a_node75"><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="-2753" rx="53.23" ry="18"/>
+<text text-anchor="middle" x="239.88" y="-2750.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="edge37" class="edge">
+<g id="edge39" class="edge">
 <title>par_red1_iff&#45;&gt;par_to_red1_or_eq</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M101.18,-2614.26C125.17,-2617.88 157.5,-2622.74 184.81,-2626.86"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="184.66,-2628.96 190.91,-2627.78 185.29,-2624.81 184.66,-2628.96"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M101.18,-2732.26C125.17,-2735.88 157.5,-2740.74 184.81,-2744.86"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="184.66,-2746.96 190.91,-2745.78 185.29,-2742.81 184.66,-2746.96"/>
 </g>
 <!-- red1_or_eq_to_par -->
-<g id="node71" class="node">
+<g id="node76" class="node">
 <title>red1_or_eq_to_par</title>
-<g id="a_node71"><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="-2583" rx="53.23" ry="18"/>
-<text text-anchor="middle" x="239.88" y="-2580.8" font-family="Inter" font-size="9.00" fill="#222222">red1_or_eq_to_par</text>
+<g id="a_node76"><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="-2701" rx="53.23" ry="18"/>
+<text text-anchor="middle" x="239.88" y="-2698.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="edge38" class="edge">
+<g id="edge40" class="edge">
 <title>par_red1_iff&#45;&gt;red1_or_eq_to_par</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M101.18,-2603.74C125.17,-2600.12 157.5,-2595.26 184.81,-2591.14"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="185.29,-2593.19 190.91,-2590.22 184.66,-2589.04 185.29,-2593.19"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M101.18,-2721.74C125.17,-2718.12 157.5,-2713.26 184.81,-2709.14"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="185.29,-2711.19 190.91,-2708.22 184.66,-2707.04 185.29,-2711.19"/>
 </g>
 <!-- red1_in_par -->
-<g id="node68" class="node">
+<g id="node73" class="node">
 <title>red1_in_par</title>
-<g id="a_node68"><a xlink:title="red1_in_par theory/Parallel.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-2661" rx="37.56" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-2658.8" font-family="Inter" font-size="9.00" fill="#222222">red1_in_par</text>
+<g id="a_node73"><a xlink:title="red1_in_par theory/Parallel.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-2779" rx="37.56" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-2776.8" font-family="Inter" font-size="9.00" fill="#222222">red1_in_par</text>
 </a>
 </g>
 </g>
 <!-- par_context -->
-<g id="node69" class="node">
+<g id="node74" class="node">
 <title>par_context</title>
-<g id="a_node69"><a xlink:title="par_context theory/Parallel.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-2713" rx="38.87" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-2710.8" font-family="Inter" font-size="9.00" fill="#222222">par_context</text>
+<g id="a_node74"><a xlink:title="par_context theory/Parallel.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-2831" rx="38.87" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-2828.8" font-family="Inter" font-size="9.00" fill="#222222">par_context</text>
 </a>
 </g>
 </g>
 <!-- par_reflexive -->
-<g id="node72" class="node">
+<g id="node77" class="node">
 <title>par_reflexive</title>
-<g id="a_node72"><a xlink:title="par_reflexive theory/Parallel.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-2765" rx="41.64" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-2762.8" font-family="Inter" font-size="9.00" fill="#222222">par_reflexive</text>
+<g id="a_node77"><a xlink:title="par_reflexive theory/Parallel.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-2883" rx="41.64" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-2880.8" font-family="Inter" font-size="9.00" fill="#222222">par_reflexive</text>
 </a>
 </g>
 </g>
 <!-- gen_list_length -->
-<g id="node73" class="node">
+<g id="node78" class="node">
 <title>gen_list_length</title>
-<g id="a_node73"><a xlink:title="gen_list_length theory/Random.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-2817" rx="46.38" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-2814.8" font-family="Inter" font-size="9.00" fill="#222222">gen_list_length</text>
+<g id="a_node78"><a xlink:title="gen_list_length theory/Random.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-2935" rx="46.38" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-2932.8" font-family="Inter" font-size="9.00" fill="#222222">gen_list_length</text>
 </a>
 </g>
 </g>
 <!-- check_term_true -->
-<g id="node74" class="node">
+<g id="node79" class="node">
 <title>check_term_true</title>
-<g id="a_node74"><a xlink:title="check_term_true theory/Random.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="921.68" cy="-741" rx="50.61" ry="18"/>
-<text text-anchor="middle" x="921.68" y="-738.8" font-family="Inter" font-size="9.00" fill="#222222">check_term_true</text>
+<g id="a_node79"><a xlink:title="check_term_true theory/Random.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="923.99" cy="-604" rx="50.61" ry="18"/>
+<text text-anchor="middle" x="923.99" y="-601.8" font-family="Inter" font-size="9.00" fill="#222222">check_term_true</text>
 </a>
 </g>
 </g>
 <!-- check_all_true -->
-<g id="node75" class="node">
+<g id="node80" class="node">
 <title>check_all_true</title>
-<g id="a_node75"><a xlink:title="check_all_true theory/Random.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="1080.15" cy="-741" rx="44.41" ry="18"/>
-<text text-anchor="middle" x="1080.15" y="-738.8" font-family="Inter" font-size="9.00" fill="#222222">check_all_true</text>
+<g id="a_node80"><a xlink:title="check_all_true theory/Random.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="1082.46" cy="-604" rx="44.41" ry="18"/>
+<text text-anchor="middle" x="1082.46" y="-601.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="edge41" class="edge">
+<g id="edge43" class="edge">
 <title>check_term_true&#45;&gt;check_all_true</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M972.62,-741C990.78,-741 1011.29,-741 1029.43,-741"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="1029.48,-743.1 1035.48,-741 1029.48,-738.9 1029.48,-743.1"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M974.92,-604C993.08,-604 1013.6,-604 1031.74,-604"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="1031.79,-606.1 1037.79,-604 1031.79,-601.9 1031.79,-606.1"/>
 </g>
 <!-- check_all_true&#45;&gt;enumerate_check -->
 <g id="edge11" class="edge">
 <title>check_all_true&#45;&gt;enumerate_check</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M1124.97,-741C1139.72,-741 1156.42,-741 1172.14,-741"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="1172.35,-743.1 1178.35,-741 1172.35,-738.9 1172.35,-743.1"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M1127.28,-604C1142.03,-604 1158.73,-604 1174.45,-604"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="1174.66,-606.1 1180.66,-604 1174.66,-601.9 1174.66,-606.1"/>
 </g>
 <!-- gen_sound -->
-<g id="node76" class="node">
+<g id="node81" class="node">
 <title>gen_sound</title>
-<g id="a_node76"><a xlink:title="gen_sound theory/Random.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="752.81" cy="-867" rx="35.59" ry="18"/>
-<text text-anchor="middle" x="752.81" y="-864.8" font-family="Inter" font-size="9.00" fill="#222222">gen_sound</text>
+<g id="a_node81"><a xlink:title="gen_sound theory/Random.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="755.12" cy="-457" rx="35.59" ry="18"/>
+<text text-anchor="middle" x="755.12" y="-454.8" font-family="Inter" font-size="9.00" fill="#222222">gen_sound</text>
 </a>
 </g>
 </g>
 <!-- gen_complete -->
-<g id="node77" class="node">
+<g id="node82" class="node">
 <title>gen_complete</title>
-<g id="a_node77"><a xlink:title="gen_complete theory/Random.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="752.81" cy="-469" rx="43.76" ry="18"/>
-<text text-anchor="middle" x="752.81" y="-466.8" font-family="Inter" font-size="9.00" fill="#222222">gen_complete</text>
+<g id="a_node82"><a xlink:title="gen_complete theory/Random.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="755.12" cy="-751" rx="43.76" ry="18"/>
+<text text-anchor="middle" x="755.12" y="-748.8" font-family="Inter" font-size="9.00" fill="#222222">gen_complete</text>
 </a>
 </g>
 </g>
 <!-- zdecs_sound -->
-<g id="node79" class="node">
+<g id="node84" class="node">
 <title>zdecs_sound</title>
-<g id="a_node79"><a xlink:title="zdecs_sound theory/Reduction.v https://arxiv.org/html/2312.13270v1">
+<g id="a_node84"><a xlink:title="zdecs_sound theory/Reduction.v https://arxiv.org/html/2312.13270v1">
 <ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-450" rx="40.98" ry="18"/>
 <text text-anchor="middle" x="239.88" y="-447.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="edge28" class="edge">
+<g id="edge30" class="edge">
 <title>zdecs_sound&#45;&gt;full_comp_aux</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M272.44,-439.05C283.39,-434.84 295.59,-429.67 306.27,-424 333.51,-409.55 362.38,-389.38 382.33,-374.58"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="383.66,-376.22 387.21,-370.94 381.14,-372.85 383.66,-376.22"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M272.82,-439.01C283.68,-434.82 295.73,-429.68 306.27,-424 333.84,-409.14 362.88,-388.2 382.8,-372.92"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="384.2,-374.49 387.66,-369.16 381.63,-371.17 384.2,-374.49"/>
 </g>
 <!-- root_steps_sound -->
-<g id="node82" class="node">
+<g id="node87" class="node">
 <title>root_steps_sound</title>
-<g id="a_node82"><a xlink:title="root_steps_sound theory/Reduction.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-729" rx="51.27" ry="18"/>
-<text text-anchor="middle" x="408.74" y="-726.8" font-family="Inter" font-size="9.00" fill="#222222">root_steps_sound</text>
+<g id="a_node87"><a xlink:title="root_steps_sound theory/Reduction.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-451" rx="51.27" ry="18"/>
+<text text-anchor="middle" x="408.74" y="-448.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="edge46" class="edge">
+<g id="edge48" class="edge">
 <title>zdecs_sound&#45;&gt;root_steps_sound</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M277.52,-457.42C288.2,-461.28 298.96,-467.14 306.27,-476 371.62,-555.21 285.52,-622.5 349.27,-703 353,-707.7 357.75,-711.58 362.93,-714.77"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="361.98,-716.64 368.24,-717.73 364.03,-712.97 361.98,-716.64"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M281.27,-450.24C302.25,-450.37 328.24,-450.52 351.19,-450.66"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="351.25,-452.76 357.26,-450.7 351.27,-448.56 351.25,-452.76"/>
 </g>
 <!-- zdecs_sound&#45;&gt;full_comp_aux_sub -->
-<g id="edge81" class="edge">
+<g id="edge83" class="edge">
 <title>zdecs_sound&#45;&gt;full_comp_aux_sub</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M276.31,-441.47C286.94,-437.54 297.96,-431.93 306.27,-424 339.8,-392 324.91,-368.43 349.27,-329 360.28,-311.19 375.19,-292.9 387.2,-279.21"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="389.07,-280.26 391.48,-274.38 385.92,-277.47 389.07,-280.26"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M276.35,-441.51C286.98,-437.58 297.99,-431.96 306.27,-424 340.26,-391.31 328.64,-369.4 349.27,-327 364.1,-296.52 382.69,-262.14 394.87,-240.05"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="396.76,-240.98 397.82,-234.71 393.08,-238.94 396.76,-240.98"/>
 </g>
 <!-- zdecs_complete -->
-<g id="node80" class="node">
+<g id="node85" class="node">
 <title>zdecs_complete</title>
-<g id="a_node80"><a xlink:title="zdecs_complete theory/Reduction.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-677" rx="49.15" ry="18"/>
-<text text-anchor="middle" x="239.88" y="-674.8" font-family="Inter" font-size="9.00" fill="#222222">zdecs_complete</text>
+<g id="a_node85"><a xlink:title="zdecs_complete theory/Reduction.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-699" rx="49.15" ry="18"/>
+<text text-anchor="middle" x="239.88" y="-696.8" font-family="Inter" font-size="9.00" fill="#222222">zdecs_complete</text>
 </a>
 </g>
 </g>
 <!-- root_steps_complete -->
-<g id="node83" class="node">
+<g id="node88" class="node">
 <title>root_steps_complete</title>
-<g id="a_node83"><a xlink:title="root_steps_complete theory/Reduction.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-677" rx="59.43" ry="18"/>
-<text text-anchor="middle" x="408.74" y="-674.8" font-family="Inter" font-size="9.00" fill="#222222">root_steps_complete</text>
+<g id="a_node88"><a xlink:title="root_steps_complete theory/Reduction.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-699" rx="59.43" ry="18"/>
+<text text-anchor="middle" x="408.74" y="-696.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="edge47" class="edge">
+<g id="edge49" class="edge">
 <title>zdecs_complete&#45;&gt;root_steps_complete</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M289.14,-677C306,-677 325.21,-677 343.19,-677"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="343.23,-679.1 349.23,-677 343.23,-674.9 343.23,-679.1"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M289.14,-699C306,-699 325.21,-699 343.19,-699"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="343.23,-701.1 349.23,-699 343.23,-696.9 343.23,-701.1"/>
 </g>
 <!-- positions_at -->
-<g id="node81" class="node">
+<g id="node86" class="node">
 <title>positions_at</title>
-<g id="a_node81"><a xlink:title="positions_at theory/Reduction.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-781" rx="38.21" ry="18"/>
-<text text-anchor="middle" x="408.74" y="-778.8" font-family="Inter" font-size="9.00" fill="#222222">positions_at</text>
+<g id="a_node86"><a xlink:title="positions_at theory/Reduction.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-507" rx="38.21" ry="18"/>
+<text text-anchor="middle" x="408.74" y="-504.8" font-family="Inter" font-size="9.00" fill="#222222">positions_at</text>
 </a>
 </g>
 </g>
 <!-- steps_sound -->
-<g id="node84" class="node">
+<g id="node89" class="node">
 <title>steps_sound</title>
-<g id="a_node84"><a xlink:title="steps_sound theory/Reduction.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="577.6" cy="-763" rx="39.02" ry="18"/>
-<text text-anchor="middle" x="577.6" y="-760.8" font-family="Inter" font-size="9.00" fill="#222222">steps_sound</text>
+<g id="a_node89"><a xlink:title="steps_sound theory/Reduction.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="578.76" cy="-507" rx="39.02" ry="18"/>
+<text text-anchor="middle" x="578.76" y="-504.8" font-family="Inter" font-size="9.00" fill="#222222">steps_sound</text>
 </a>
 </g>
 </g>
 <!-- positions_at&#45;&gt;steps_sound -->
-<g id="edge48" class="edge">
+<g id="edge50" class="edge">
 <title>positions_at&#45;&gt;steps_sound</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M445.95,-777.09C471.61,-774.33 506.16,-770.6 533.29,-767.67"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="533.57,-769.75 539.31,-767.02 533.12,-765.58 533.57,-769.75"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M447.03,-507C472.45,-507 506.23,-507 533.09,-507"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="533.41,-509.1 539.41,-507 533.41,-504.9 533.41,-509.1"/>
 </g>
 <!-- root_steps_sound&#45;&gt;steps_sound -->
-<g id="edge49" class="edge">
+<g id="edge51" class="edge">
 <title>root_steps_sound&#45;&gt;steps_sound</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M453.58,-737.93C478.86,-743.08 510.45,-749.52 535.29,-754.58"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="535.16,-756.7 541.46,-755.84 536,-752.58 535.16,-756.7"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M446.61,-463.29C474.57,-472.61 512.82,-485.36 540.8,-494.68"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="540.25,-496.71 546.61,-496.62 541.58,-492.73 540.25,-496.71"/>
 </g>
 <!-- steps_complete -->
-<g id="node91" class="node">
+<g id="node96" class="node">
 <title>steps_complete</title>
-<g id="a_node91"><a xlink:title="steps_complete theory/Reduction.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="577.6" cy="-573" rx="47.84" ry="18"/>
-<text text-anchor="middle" x="577.6" y="-570.8" font-family="Inter" font-size="9.00" fill="#222222">steps_complete</text>
+<g id="a_node96"><a xlink:title="steps_complete theory/Reduction.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="578.76" cy="-699" rx="47.84" ry="18"/>
+<text text-anchor="middle" x="578.76" y="-696.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="edge55" class="edge">
+<g id="edge57" class="edge">
 <title>root_steps_complete&#45;&gt;steps_complete</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M445.25,-662.61C452.97,-659.1 460.98,-655.15 468.21,-651 498.36,-633.69 530.39,-609.89 551.74,-593.15"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="553.26,-594.63 556.67,-589.26 550.65,-591.33 553.26,-594.63"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M468.5,-699C486.62,-699 506.47,-699 524.22,-699"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="524.66,-701.1 530.66,-699 524.66,-696.9 524.66,-701.1"/>
 </g>
 <!-- steps_sound&#45;&gt;enumerate_sound -->
 <g id="edge12" class="edge">
 <title>steps_sound&#45;&gt;enumerate_sound</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M610.78,-753.34C637.74,-745.25 676.55,-733.6 706.63,-724.56"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="707.38,-726.53 712.52,-722.8 706.17,-722.51 707.38,-726.53"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M618.02,-507.44C640.76,-507.7 670.06,-508.04 695.65,-508.33"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="695.7,-510.43 701.73,-508.4 695.75,-506.23 695.7,-510.43"/>
 </g>
 <!-- steps_sound&#45;&gt;gen_sound -->
-<g id="edge42" class="edge">
+<g id="edge44" class="edge">
 <title>steps_sound&#45;&gt;gen_sound</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M597.63,-778.88C618.56,-795.82 653.68,-822.68 687,-841 696.41,-846.18 707.07,-850.88 716.99,-854.83"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="716.38,-856.84 722.73,-857.06 717.9,-852.93 716.38,-856.84"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M612.55,-497.6C642.43,-489.03 686.48,-476.4 717.5,-467.5"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="718.33,-469.45 723.52,-465.78 717.17,-465.41 718.33,-469.45"/>
 </g>
 <!-- steps_sound_red1 -->
-<g id="node85" class="node">
+<g id="node90" class="node">
 <title>steps_sound_red1</title>
-<g id="a_node85"><a xlink:title="steps_sound_red1 theory/Reduction.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="752.81" cy="-763" rx="51.92" ry="18"/>
-<text text-anchor="middle" x="752.81" y="-760.8" font-family="Inter" font-size="9.00" fill="#222222">steps_sound_red1</text>
+<g id="a_node90"><a xlink:title="steps_sound_red1 theory/Reduction.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="755.12" cy="-647" rx="51.92" ry="18"/>
+<text text-anchor="middle" x="755.12" y="-644.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="edge50" class="edge">
+<g id="edge52" class="edge">
 <title>steps_sound&#45;&gt;steps_sound_red1</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M617.04,-763C639.83,-763 669.15,-763 694.62,-763"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="694.66,-765.1 700.66,-763 694.66,-760.9 694.66,-765.1"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M611.89,-516.93C623.39,-521.38 636.04,-527.37 646.31,-535 670.38,-552.89 668.7,-565.21 689.31,-587 702.26,-600.69 717.71,-615.07 730.28,-626.31"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="728.89,-627.89 734.77,-630.31 731.68,-624.75 728.89,-627.89"/>
 </g>
 <!-- has_red_spec -->
-<g id="node93" class="node">
+<g id="node98" class="node">
 <title>has_red_spec</title>
-<g id="a_node93"><a xlink:title="has_red_spec theory/Reduction.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="752.81" cy="-659" rx="42.95" ry="18"/>
-<text text-anchor="middle" x="752.81" y="-656.8" font-family="Inter" font-size="9.00" fill="#222222">has_red_spec</text>
+<g id="a_node98"><a xlink:title="has_red_spec theory/Reduction.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="755.12" cy="-561" rx="42.95" ry="18"/>
+<text text-anchor="middle" x="755.12" y="-558.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="edge59" class="edge">
+<g id="edge61" class="edge">
 <title>steps_sound&#45;&gt;has_red_spec</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M597.63,-747.12C618.56,-730.18 653.68,-703.32 687,-685 695.28,-680.45 704.52,-676.26 713.38,-672.63"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="714.34,-674.51 719.13,-670.33 712.78,-670.61 714.34,-674.51"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M611.74,-516.9C640.59,-525.84 683.14,-539.02 714.21,-548.64"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="713.91,-550.74 720.26,-550.51 715.15,-546.73 713.91,-550.74"/>
 </g>
 <!-- corpus_sound -->
-<g id="node128" class="node">
+<g id="node133" class="node">
 <title>corpus_sound</title>
-<g id="a_node128"><a xlink:title="corpus_sound theory/Tests.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="752.81" cy="-815" rx="43.1" ry="18"/>
-<text text-anchor="middle" x="752.81" y="-812.8" font-family="Inter" font-size="9.00" fill="#222222">corpus_sound</text>
+<g id="a_node133"><a xlink:title="corpus_sound theory/Tests.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="755.12" cy="-405" rx="43.1" ry="18"/>
+<text text-anchor="middle" x="755.12" y="-402.8" font-family="Inter" font-size="9.00" fill="#222222">corpus_sound</text>
 </a>
 </g>
 </g>
 <!-- steps_sound&#45;&gt;corpus_sound -->
-<g id="edge88" class="edge">
+<g id="edge90" class="edge">
 <title>steps_sound&#45;&gt;corpus_sound</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M610.78,-772.66C639.12,-781.17 680.54,-793.6 711.16,-802.8"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="710.79,-804.88 717.14,-804.59 712,-800.85 710.79,-804.88"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M599.08,-491.58C620.32,-475.13 655.88,-449 689.31,-431 697.62,-426.52 706.89,-422.36 715.74,-418.74"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="716.7,-420.61 721.49,-416.44 715.14,-416.71 716.7,-420.61"/>
 </g>
 <!-- steps_sound_red1&#45;&gt;check_term_true -->
-<g id="edge40" class="edge">
+<g id="edge42" class="edge">
 <title>steps_sound_red1&#45;&gt;check_term_true</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M801.63,-756.7C822.23,-753.98 846.39,-750.79 867.55,-748"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="868.04,-750.06 873.72,-747.19 867.5,-745.89 868.04,-750.06"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M797.37,-636.37C821.4,-630.18 851.78,-622.35 876.64,-615.94"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="877.22,-617.96 882.5,-614.43 876.17,-613.9 877.22,-617.96"/>
 </g>
 <!-- steps_sound_red1&#45;&gt;gen_fv_preserved -->
-<g id="edge45" class="edge">
+<g id="edge47" class="edge">
 <title>steps_sound_red1&#45;&gt;gen_fv_preserved</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M787.46,-776.49C797.49,-780.51 808.51,-784.93 818.63,-789 839.19,-797.25 862.06,-806.44 880.94,-814.03"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="880.31,-816.04 886.66,-816.33 881.88,-812.14 880.31,-816.04"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M792.68,-659.48C802.15,-663.29 812.15,-667.86 820.94,-673 850.73,-690.42 881.08,-716.02 900.84,-733.97"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="899.54,-735.63 905.39,-738.13 902.38,-732.53 899.54,-735.63"/>
 </g>
 <!-- nf_iff_steps_nil -->
-<g id="node95" class="node">
+<g id="node100" class="node">
 <title>nf_iff_steps_nil</title>
-<g id="a_node95"><a xlink:title="nf_iff_steps_nil theory/Reduction.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="921.68" cy="-637" rx="45.07" ry="18"/>
-<text text-anchor="middle" x="921.68" y="-634.8" font-family="Inter" font-size="9.00" fill="#222222">nf_iff_steps_nil</text>
+<g id="a_node100"><a xlink:title="nf_iff_steps_nil theory/Reduction.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="923.99" cy="-656" rx="45.07" ry="18"/>
+<text text-anchor="middle" x="923.99" y="-653.8" font-family="Inter" font-size="9.00" fill="#222222">nf_iff_steps_nil</text>
 </a>
 </g>
 </g>
 <!-- steps_sound_red1&#45;&gt;nf_iff_steps_nil -->
-<g id="edge62" class="edge">
+<g id="edge64" class="edge">
 <title>steps_sound_red1&#45;&gt;nf_iff_steps_nil</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M793.87,-751.74C802.67,-748.02 811.48,-743.19 818.63,-737 847.41,-712.12 833.28,-688.36 861.63,-663 867.05,-658.16 873.51,-654.1 880.13,-650.74"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="881.21,-652.56 885.72,-648.08 879.4,-648.77 881.21,-652.56"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M806.64,-649.72C827.68,-650.86 852.05,-652.17 873.03,-653.31"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="873.03,-655.41 879.14,-653.63 873.26,-651.21 873.03,-655.41"/>
 </g>
 <!-- steps_sound_red1&#45;&gt;corpus_fv_preserved -->
-<g id="edge92" class="edge">
+<g id="edge94" class="edge">
 <title>steps_sound_red1&#45;&gt;corpus_fv_preserved</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M793.34,-774.35C802.25,-778.08 811.25,-782.9 818.63,-789 845.9,-811.55 837.5,-830.12 861.63,-856 869.95,-864.92 880.26,-873.3 889.93,-880.3"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="888.81,-882.08 894.92,-883.84 891.24,-878.65 888.81,-882.08"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M797.21,-657.66C805.86,-661.4 814.35,-666.39 820.94,-673 857.43,-709.58 833.77,-739.06 863.94,-781 871.96,-792.15 883,-802.37 893.36,-810.63"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="892.35,-812.5 898.37,-814.52 894.92,-809.18 892.35,-812.5"/>
 </g>
 <!-- positions_hole -->
-<g id="node86" class="node">
+<g id="node91" class="node">
 <title>positions_hole</title>
-<g id="a_node86"><a xlink:title="positions_hole theory/Reduction.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-502" rx="44.41" ry="18"/>
-<text text-anchor="middle" x="239.88" y="-499.8" font-family="Inter" font-size="9.00" fill="#222222">positions_hole</text>
+<g id="a_node91"><a xlink:title="positions_hole theory/Reduction.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-647" rx="44.41" ry="18"/>
+<text text-anchor="middle" x="239.88" y="-644.8" font-family="Inter" font-size="9.00" fill="#222222">positions_hole</text>
 </a>
 </g>
 </g>
 <!-- root_steps_in_steps -->
-<g id="node87" class="node">
+<g id="node92" class="node">
 <title>root_steps_in_steps</title>
-<g id="a_node87"><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="-469" rx="56.66" ry="18"/>
-<text text-anchor="middle" x="408.74" y="-466.8" font-family="Inter" font-size="9.00" fill="#222222">root_steps_in_steps</text>
+<g id="a_node92"><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="-647" rx="56.66" ry="18"/>
+<text text-anchor="middle" x="408.74" y="-644.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="edge51" class="edge">
+<g id="edge53" class="edge">
 <title>positions_hole&#45;&gt;root_steps_in_steps</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M280.42,-494.18C302.45,-489.82 330.2,-484.34 354.16,-479.6"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="354.68,-481.63 360.16,-478.41 353.87,-477.51 354.68,-481.63"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M284.72,-647C303.36,-647 325.43,-647 345.69,-647"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="345.92,-649.1 351.92,-647 345.92,-644.9 345.92,-649.1"/>
 </g>
 <!-- root_steps_in_steps&#45;&gt;steps_complete -->
-<g id="edge56" class="edge">
+<g id="edge58" class="edge">
 <title>root_steps_in_steps&#45;&gt;steps_complete</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M444.64,-483.11C452.54,-486.69 460.79,-490.74 468.21,-495 498.36,-512.31 530.39,-536.11 551.74,-552.85"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="550.65,-554.67 556.67,-556.74 553.26,-551.37 550.65,-554.67"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M449.98,-659.46C475.8,-667.44 509.26,-677.8 535.46,-685.91"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="534.92,-687.94 541.28,-687.71 536.17,-683.93 534.92,-687.94"/>
 </g>
 <!-- plug_comp -->
-<g id="node88" class="node">
+<g id="node93" class="node">
 <title>plug_comp</title>
-<g id="a_node88"><a xlink:title="plug_comp theory/Reduction.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-625" rx="35.59" ry="18"/>
-<text text-anchor="middle" x="408.74" y="-622.8" font-family="Inter" font-size="9.00" fill="#222222">plug_comp</text>
+<g id="a_node93"><a xlink:title="plug_comp theory/Reduction.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-803" rx="35.59" ry="18"/>
+<text text-anchor="middle" x="408.74" y="-800.8" font-family="Inter" font-size="9.00" fill="#222222">plug_comp</text>
 </a>
 </g>
 </g>
 <!-- plug_comp&#45;&gt;steps_complete -->
-<g id="edge53" class="edge">
+<g id="edge55" class="edge">
 <title>plug_comp&#45;&gt;steps_complete</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M439.57,-615.7C465.94,-607.49 504.68,-595.41 534.25,-586.2"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="534.94,-588.18 540.04,-584.39 533.69,-584.17 534.94,-588.18"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M437.37,-792.06C447.3,-787.78 458.46,-782.56 468.21,-777 498.62,-759.64 531,-735.85 552.6,-719.12"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="554.14,-720.59 557.58,-715.24 551.56,-717.27 554.14,-720.59"/>
 </g>
 <!-- positions_comp -->
-<g id="node89" class="node">
+<g id="node94" class="node">
 <title>positions_comp</title>
-<g id="a_node89"><a xlink:title="positions_comp theory/Reduction.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-573" rx="47.19" ry="18"/>
-<text text-anchor="middle" x="408.74" y="-570.8" font-family="Inter" font-size="9.00" fill="#222222">positions_comp</text>
+<g id="a_node94"><a xlink:title="positions_comp theory/Reduction.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-751" rx="47.19" ry="18"/>
+<text text-anchor="middle" x="408.74" y="-748.8" font-family="Inter" font-size="9.00" fill="#222222">positions_comp</text>
 </a>
 </g>
 </g>
 <!-- positions_comp&#45;&gt;steps_complete -->
-<g id="edge54" class="edge">
+<g id="edge56" class="edge">
 <title>positions_comp&#45;&gt;steps_complete</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M456.22,-573C477.11,-573 501.87,-573 523.49,-573"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="523.5,-575.1 529.5,-573 523.5,-570.9 523.5,-575.1"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M446.2,-739.72C472.51,-731.57 508.1,-720.56 535.62,-712.04"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="536.26,-714.04 541.37,-710.26 535.02,-710.03 536.26,-714.04"/>
 </g>
 <!-- at_ctx_comp -->
-<g id="node90" class="node">
+<g id="node95" class="node">
 <title>at_ctx_comp</title>
-<g id="a_node90"><a xlink:title="at_ctx_comp theory/Reduction.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-521" rx="40.33" ry="18"/>
-<text text-anchor="middle" x="408.74" y="-518.8" font-family="Inter" font-size="9.00" fill="#222222">at_ctx_comp</text>
+<g id="a_node95"><a xlink:title="at_ctx_comp theory/Reduction.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-595" rx="40.33" ry="18"/>
+<text text-anchor="middle" x="408.74" y="-592.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="edge52" class="edge">
+<g id="edge54" class="edge">
 <title>at_ctx_comp&#45;&gt;steps_complete</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M442.31,-531.15C468.52,-539.32 505.56,-550.86 534.1,-559.75"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="533.7,-561.83 540.05,-561.61 534.95,-557.82 533.7,-561.83"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M439.45,-606.84C448.84,-610.94 459.14,-615.82 468.21,-621 498.62,-638.36 531,-662.15 552.6,-678.88"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="551.56,-680.73 557.58,-682.76 554.14,-677.41 551.56,-680.73"/>
 </g>
 <!-- steps_complete&#45;&gt;enumerate_complete -->
 <g id="edge13" class="edge">
 <title>steps_complete&#45;&gt;enumerate_complete</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M615.76,-561.84C641.37,-554.16 675.67,-543.86 703.41,-535.53"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="704.09,-537.52 709.23,-533.78 702.88,-533.5 704.09,-537.52"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M599.79,-715.49C621.06,-732.45 656.12,-758.86 689.31,-777 695.71,-780.5 702.68,-783.79 709.6,-786.77"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="709.04,-788.82 715.39,-789.21 710.67,-784.95 709.04,-788.82"/>
 </g>
 <!-- steps_complete&#45;&gt;gen_complete -->
-<g id="edge43" class="edge">
+<g id="edge45" class="edge">
 <title>steps_complete&#45;&gt;gen_complete</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M598.4,-556.49C619.42,-539.52 654.08,-513.09 687,-495 695.19,-490.5 704.33,-486.35 713.1,-482.75"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="714.01,-484.64 718.79,-480.46 712.44,-480.75 714.01,-484.64"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M616.73,-710.03C645.01,-718.46 683.98,-730.08 713.2,-738.8"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="712.93,-740.91 719.28,-740.61 714.13,-736.88 712.93,-740.91"/>
 </g>
 <!-- steps_complete&#45;&gt;has_red_spec -->
-<g id="edge58" class="edge">
+<g id="edge60" class="edge">
 <title>steps_complete&#45;&gt;has_red_spec</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M606.06,-587.6C627.87,-599.1 659.22,-615.4 687,-629 696.77,-633.78 707.46,-638.82 717.29,-643.36"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="716.64,-645.37 722.97,-645.97 718.4,-641.56 716.64,-645.37"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M593.84,-681.79C613.38,-658.78 650.67,-617.77 689.31,-591 697.83,-585.1 707.69,-579.85 717.12,-575.46"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="718.01,-577.36 722.61,-572.98 716.27,-573.54 718.01,-577.36"/>
 </g>
 <!-- steps_complete&#45;&gt;nf_iff_steps_nil -->
-<g id="edge61" class="edge">
+<g id="edge63" class="edge">
 <title>steps_complete&#45;&gt;nf_iff_steps_nil</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M617.58,-583.09C638.15,-588.23 663.85,-594.35 687,-599 750.82,-611.83 825.12,-623.33 872.5,-630.23"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="872.48,-632.35 878.72,-631.14 873.08,-628.2 872.48,-632.35"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M596.45,-681.92C616.44,-662.8 651.94,-632.94 689.31,-621 757.13,-599.32 840.41,-623.13 887.01,-640.71"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="886.42,-642.74 892.78,-642.93 887.93,-638.82 886.42,-642.74"/>
 </g>
 <!-- corpus_complete -->
-<g id="node129" class="node">
+<g id="node134" class="node">
 <title>corpus_complete</title>
-<g id="a_node129"><a xlink:title="corpus_complete theory/Tests.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="752.81" cy="-573" rx="51.27" ry="18"/>
-<text text-anchor="middle" x="752.81" y="-570.8" font-family="Inter" font-size="9.00" fill="#222222">corpus_complete</text>
+<g id="a_node134"><a xlink:title="corpus_complete theory/Tests.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="755.12" cy="-699" rx="51.27" ry="18"/>
+<text text-anchor="middle" x="755.12" y="-696.8" font-family="Inter" font-size="9.00" fill="#222222">corpus_complete</text>
 </a>
 </g>
 </g>
 <!-- steps_complete&#45;&gt;corpus_complete -->
-<g id="edge89" class="edge">
+<g id="edge91" class="edge">
 <title>steps_complete&#45;&gt;corpus_complete</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M625.93,-573C647.27,-573 672.63,-573 694.99,-573"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="695.2,-575.1 701.2,-573 695.2,-570.9 695.2,-575.1"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M626.94,-699C648.7,-699 674.7,-699 697.51,-699"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="697.54,-701.1 703.54,-699 697.54,-696.9 697.54,-701.1"/>
 </g>
 <!-- has_red_f -->
-<g id="node92" class="node">
+<g id="node97" class="node">
 <title>has_red_f</title>
-<g id="a_node92"><a xlink:title="has_red_f theory/Reduction.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="577.6" cy="-659" rx="32.16" ry="18"/>
-<text text-anchor="middle" x="577.6" y="-656.8" font-family="Inter" font-size="9.00" fill="#222222">has_red_f</text>
+<g id="a_node97"><a xlink:title="has_red_f theory/Reduction.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="578.76" cy="-561" rx="32.16" ry="18"/>
+<text text-anchor="middle" x="578.76" y="-558.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="edge57" class="edge">
+<g id="edge59" class="edge">
 <title>has_red_f&#45;&gt;has_red_spec</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M609.97,-659C636.09,-659 673.72,-659 703.66,-659"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="703.92,-661.1 709.92,-659 703.92,-656.9 703.92,-661.1"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M611.33,-561C637.72,-561 675.77,-561 705.96,-561"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="706.28,-563.1 712.28,-561 706.28,-558.9 706.28,-563.1"/>
 </g>
 <!-- has_red_spec&#45;&gt;check_term_true -->
-<g id="edge39" class="edge">
+<g id="edge41" class="edge">
 <title>has_red_spec&#45;&gt;check_term_true</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M786.12,-670.29C796.72,-674.43 808.39,-679.47 818.63,-685 839.13,-696.08 841.32,-703.58 861.63,-715 867.96,-718.56 874.88,-721.98 881.67,-725.11"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="881,-727.11 887.33,-727.67 882.73,-723.28 881,-727.11"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M791.92,-570.22C816.58,-576.58 849.59,-585.09 876.31,-591.97"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="875.93,-594.04 882.26,-593.51 876.98,-589.97 875.93,-594.04"/>
 </g>
 <!-- red1_dec -->
-<g id="node94" class="node">
+<g id="node99" class="node">
 <title>red1_dec</title>
-<g id="a_node94"><a xlink:title="red1_dec theory/Reduction.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="921.68" cy="-689" rx="30.7" ry="18"/>
-<text text-anchor="middle" x="921.68" y="-686.8" font-family="Inter" font-size="9.00" fill="#222222">red1_dec</text>
+<g id="a_node99"><a xlink:title="red1_dec theory/Reduction.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="923.99" cy="-500" rx="30.7" ry="18"/>
+<text text-anchor="middle" x="923.99" y="-497.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="edge60" class="edge">
+<g id="edge62" class="edge">
 <title>has_red_spec&#45;&gt;red1_dec</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M792.52,-665.96C820.8,-671.04 858.82,-677.88 886.09,-682.78"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="885.81,-684.86 892.09,-683.86 886.55,-680.73 885.81,-684.86"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M787.9,-549.38C817.78,-538.46 862.22,-522.22 891.87,-511.37"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="892.68,-513.31 897.6,-509.28 891.24,-509.37 892.68,-513.31"/>
 </g>
 <!-- corpus_decides -->
-<g id="node130" class="node">
+<g id="node135" class="node">
 <title>corpus_decides</title>
-<g id="a_node130"><a xlink:title="corpus_decides theory/Tests.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="921.68" cy="-585" rx="47.84" ry="18"/>
-<text text-anchor="middle" x="921.68" y="-582.8" font-family="Inter" font-size="9.00" fill="#222222">corpus_decides</text>
+<g id="a_node135"><a xlink:title="corpus_decides theory/Tests.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="923.99" cy="-552" rx="47.84" ry="18"/>
+<text text-anchor="middle" x="923.99" y="-549.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="edge90" class="edge">
+<g id="edge92" class="edge">
 <title>has_red_spec&#45;&gt;corpus_decides</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M783.09,-645.93C804.76,-636.26 835.03,-622.78 861.63,-611 868.9,-607.78 876.67,-604.35 884.11,-601.08"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="885.07,-602.95 889.72,-598.61 883.38,-599.1 885.07,-602.95"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M797.8,-558.75C819.69,-557.57 846.74,-556.11 870.09,-554.85"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="870.38,-556.94 876.26,-554.52 870.15,-552.75 870.38,-556.94"/>
 </g>
 <!-- normal_form_iff_nf -->
-<g id="node96" class="node">
+<g id="node101" class="node">
 <title>normal_form_iff_nf</title>
-<g id="a_node96"><a xlink:title="normal_form_iff_nf theory/Reduction.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="1080.15" cy="-611" rx="55.35" ry="18"/>
-<text text-anchor="middle" x="1080.15" y="-608.8" font-family="Inter" font-size="9.00" fill="#222222">normal_form_iff_nf</text>
+<g id="a_node101"><a xlink:title="normal_form_iff_nf theory/Reduction.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="1082.46" cy="-708" rx="55.35" ry="18"/>
+<text text-anchor="middle" x="1082.46" y="-705.8" font-family="Inter" font-size="9.00" fill="#222222">normal_form_iff_nf</text>
 </a>
 </g>
 </g>
 <!-- nf_iff_steps_nil&#45;&gt;normal_form_iff_nf -->
-<g id="edge63" class="edge">
+<g id="edge65" class="edge">
 <title>nf_iff_steps_nil&#45;&gt;normal_form_iff_nf</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M963.79,-630.17C982.33,-627.09 1004.5,-623.4 1024.42,-620.09"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="1024.96,-622.13 1030.53,-619.08 1024.27,-617.99 1024.96,-622.13"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M959.32,-667.41C982.23,-675.02 1012.55,-685.1 1037.25,-693.31"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="1036.72,-695.35 1043.08,-695.25 1038.05,-691.36 1036.72,-695.35"/>
 </g>
 <!-- nf_dec -->
-<g id="node97" class="node">
+<g id="node102" class="node">
 <title>nf_dec</title>
-<g id="a_node97"><a xlink:title="nf_dec theory/Reduction.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="1080.15" cy="-663" rx="27" ry="18"/>
-<text text-anchor="middle" x="1080.15" y="-660.8" font-family="Inter" font-size="9.00" fill="#222222">nf_dec</text>
+<g id="a_node102"><a xlink:title="nf_dec theory/Reduction.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="1082.46" cy="-656" rx="27" ry="18"/>
+<text text-anchor="middle" x="1082.46" y="-653.8" font-family="Inter" font-size="9.00" fill="#222222">nf_dec</text>
 </a>
 </g>
 </g>
 <!-- nf_iff_steps_nil&#45;&gt;nf_dec -->
-<g id="edge64" class="edge">
+<g id="edge66" class="edge">
 <title>nf_iff_steps_nil&#45;&gt;nf_dec</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M963.79,-643.83C990,-648.19 1023.44,-653.74 1047.57,-657.75"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="1047.23,-659.82 1053.49,-658.74 1047.92,-655.68 1047.23,-659.82"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M969.41,-656C994.68,-656 1025.78,-656 1048.8,-656"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="1049.06,-658.1 1055.06,-656 1049.06,-653.9 1049.06,-658.1"/>
 </g>
 <!-- open_rec_app -->
-<g id="node98" class="node">
+<g id="node103" class="node">
 <title>open_rec_app</title>
-<g id="a_node98"><a xlink:title="open_rec_app theory/Substitution.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-2869" rx="43.1" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-2866.8" font-family="Inter" font-size="9.00" fill="#222222">open_rec_app</text>
+<g id="a_node103"><a xlink:title="open_rec_app theory/Substitution.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-2987" rx="43.1" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-2984.8" font-family="Inter" font-size="9.00" fill="#222222">open_rec_app</text>
 </a>
 </g>
 </g>
 <!-- open_rec_lam -->
-<g id="node99" class="node">
+<g id="node104" class="node">
 <title>open_rec_lam</title>
-<g id="a_node99"><a xlink:title="open_rec_lam theory/Substitution.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-2921" rx="43.76" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-2918.8" font-family="Inter" font-size="9.00" fill="#222222">open_rec_lam</text>
+<g id="a_node104"><a xlink:title="open_rec_lam theory/Substitution.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-3039" rx="43.76" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-3036.8" font-family="Inter" font-size="9.00" fill="#222222">open_rec_lam</text>
 </a>
 </g>
 </g>
 <!-- open_rec_esub -->
-<g id="node100" class="node">
+<g id="node105" class="node">
 <title>open_rec_esub</title>
-<g id="a_node100"><a xlink:title="open_rec_esub theory/Substitution.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-2973" rx="46.38" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-2970.8" font-family="Inter" font-size="9.00" fill="#222222">open_rec_esub</text>
+<g id="a_node105"><a xlink:title="open_rec_esub theory/Substitution.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-3091" rx="46.38" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-3088.8" font-family="Inter" font-size="9.00" fill="#222222">open_rec_esub</text>
 </a>
 </g>
 </g>
 <!-- close_rec_app -->
-<g id="node101" class="node">
+<g id="node106" class="node">
 <title>close_rec_app</title>
-<g id="a_node101"><a xlink:title="close_rec_app theory/Substitution.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-3025" rx="44.41" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-3022.8" font-family="Inter" font-size="9.00" fill="#222222">close_rec_app</text>
+<g id="a_node106"><a xlink:title="close_rec_app theory/Substitution.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-3143" rx="44.41" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-3140.8" font-family="Inter" font-size="9.00" fill="#222222">close_rec_app</text>
 </a>
 </g>
 </g>
 <!-- close_rec_lam -->
-<g id="node102" class="node">
+<g id="node107" class="node">
 <title>close_rec_lam</title>
-<g id="a_node102"><a xlink:title="close_rec_lam theory/Substitution.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-3077" rx="44.41" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-3074.8" font-family="Inter" font-size="9.00" fill="#222222">close_rec_lam</text>
+<g id="a_node107"><a xlink:title="close_rec_lam theory/Substitution.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-3195" rx="44.41" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-3192.8" font-family="Inter" font-size="9.00" fill="#222222">close_rec_lam</text>
 </a>
 </g>
 </g>
 <!-- close_rec_esub -->
-<g id="node103" class="node">
+<g id="node108" class="node">
 <title>close_rec_esub</title>
-<g id="a_node103"><a xlink:title="close_rec_esub theory/Substitution.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-3129" rx="46.53" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-3126.8" font-family="Inter" font-size="9.00" fill="#222222">close_rec_esub</text>
+<g id="a_node108"><a xlink:title="close_rec_esub theory/Substitution.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-3247" rx="46.53" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-3244.8" font-family="Inter" font-size="9.00" fill="#222222">close_rec_esub</text>
 </a>
 </g>
 </g>
 <!-- subst_app -->
-<g id="node104" class="node">
+<g id="node109" class="node">
 <title>subst_app</title>
-<g id="a_node104"><a xlink:title="subst_app theory/Substitution.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-3181" rx="34.13" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-3178.8" font-family="Inter" font-size="9.00" fill="#222222">subst_app</text>
+<g id="a_node109"><a xlink:title="subst_app theory/Substitution.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-3299" rx="34.13" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-3296.8" font-family="Inter" font-size="9.00" fill="#222222">subst_app</text>
 </a>
 </g>
 </g>
 <!-- subst_lam -->
-<g id="node105" class="node">
+<g id="node110" class="node">
 <title>subst_lam</title>
-<g id="a_node105"><a xlink:title="subst_lam theory/Substitution.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-3233" rx="34.13" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-3230.8" font-family="Inter" font-size="9.00" fill="#222222">subst_lam</text>
+<g id="a_node110"><a xlink:title="subst_lam theory/Substitution.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-3351" rx="34.13" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-3348.8" font-family="Inter" font-size="9.00" fill="#222222">subst_lam</text>
 </a>
 </g>
 </g>
 <!-- subst_esub -->
-<g id="node106" class="node">
+<g id="node111" class="node">
 <title>subst_esub</title>
-<g id="a_node106"><a xlink:title="subst_esub theory/Substitution.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-3285" rx="36.25" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-3282.8" font-family="Inter" font-size="9.00" fill="#222222">subst_esub</text>
+<g id="a_node111"><a xlink:title="subst_esub theory/Substitution.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-3403" rx="36.25" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-3400.8" font-family="Inter" font-size="9.00" fill="#222222">subst_esub</text>
 </a>
 </g>
 </g>
 <!-- open_rec_lc_atom -->
-<g id="node110" class="node">
+<g id="node115" class="node">
 <title>open_rec_lc_atom</title>
-<g id="a_node110"><a xlink:title="open_rec_lc_atom theory/Substitution.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-3337" rx="53.89" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-3334.8" font-family="Inter" font-size="9.00" fill="#222222">open_rec_lc_atom</text>
+<g id="a_node115"><a xlink:title="open_rec_lc_atom theory/Substitution.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-3455" rx="53.89" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-3452.8" font-family="Inter" font-size="9.00" fill="#222222">open_rec_lc_atom</text>
 </a>
 </g>
 </g>
 <!-- open_rec_lc -->
-<g id="node111" class="node">
+<g id="node116" class="node">
 <title>open_rec_lc</title>
-<g id="a_node111"><a xlink:title="open_rec_lc theory/Substitution.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-3337" rx="39.02" ry="18"/>
-<text text-anchor="middle" x="239.88" y="-3334.8" font-family="Inter" font-size="9.00" fill="#222222">open_rec_lc</text>
+<g id="a_node116"><a xlink:title="open_rec_lc theory/Substitution.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-3455" rx="39.02" ry="18"/>
+<text text-anchor="middle" x="239.88" y="-3452.8" font-family="Inter" font-size="9.00" fill="#222222">open_rec_lc</text>
 </a>
 </g>
 </g>
 <!-- open_rec_lc_atom&#45;&gt;open_rec_lc -->
-<g id="edge69" class="edge">
+<g id="edge71" class="edge">
 <title>open_rec_lc_atom&#45;&gt;open_rec_lc</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M118.98,-3337C143.1,-3337 171.36,-3337 194.39,-3337"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="194.43,-3339.1 200.43,-3337 194.43,-3334.9 194.43,-3339.1"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M118.98,-3455C143.1,-3455 171.36,-3455 194.39,-3455"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="194.43,-3457.1 200.43,-3455 194.43,-3452.9 194.43,-3457.1"/>
 </g>
 <!-- red_sub_root_to_red1 -->
-<g id="node112" class="node">
+<g id="node117" class="node">
 <title>red_sub_root_to_red1</title>
-<g id="a_node112"><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="-3389" rx="60.09" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-3386.8" font-family="Inter" font-size="9.00" fill="#222222">red_sub_root_to_red1</text>
+<g id="a_node117"><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="-3507" rx="60.09" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-3504.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="node113" class="node">
+<g id="node118" class="node">
 <title>red_sub_to_red1</title>
-<g id="a_node113"><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="-3389" rx="47.84" ry="18"/>
-<text text-anchor="middle" x="239.88" y="-3386.8" font-family="Inter" font-size="9.00" fill="#222222">red_sub_to_red1</text>
+<g id="a_node118"><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="-3507" rx="47.84" ry="18"/>
+<text text-anchor="middle" x="239.88" y="-3504.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="edge70" class="edge">
+<g id="edge72" 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,-3389C145.11,-3389 166.58,-3389 185.56,-3389"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="185.89,-3391.1 191.89,-3389 185.89,-3386.9 185.89,-3391.1"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M125.65,-3507C145.11,-3507 166.58,-3507 185.56,-3507"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="185.89,-3509.1 191.89,-3507 185.89,-3504.9 185.89,-3509.1"/>
 </g>
 <!-- red_sub_context -->
-<g id="node114" class="node">
+<g id="node119" class="node">
 <title>red_sub_context</title>
-<g id="a_node114"><a xlink:title="red_sub_context theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-3441" rx="49.15" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-3438.8" font-family="Inter" font-size="9.00" fill="#222222">red_sub_context</text>
+<g id="a_node119"><a xlink:title="red_sub_context theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-3559" rx="49.15" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-3556.8" font-family="Inter" font-size="9.00" fill="#222222">red_sub_context</text>
 </a>
 </g>
 </g>
 <!-- Star_red_sub_context -->
-<g id="node120" class="node">
+<g id="node125" class="node">
 <title>Star_red_sub_context</title>
-<g id="a_node120"><a xlink:title="Star_red_sub_context theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-3441" rx="61.55" ry="18"/>
-<text text-anchor="middle" x="239.88" y="-3438.8" font-family="Inter" font-size="9.00" fill="#222222">Star_red_sub_context</text>
+<g id="a_node125"><a xlink:title="Star_red_sub_context theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-3559" rx="61.55" ry="18"/>
+<text text-anchor="middle" x="239.88" y="-3556.8" font-family="Inter" font-size="9.00" fill="#222222">Star_red_sub_context</text>
 </a>
 </g>
 </g>
 <!-- red_sub_context&#45;&gt;Star_red_sub_context -->
-<g id="edge73" class="edge">
+<g id="edge75" class="edge">
 <title>red_sub_context&#45;&gt;Star_red_sub_context</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M114.33,-3441C132.08,-3441 152.53,-3441 171.66,-3441"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="172.09,-3443.1 178.09,-3441 172.09,-3438.9 172.09,-3443.1"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M114.33,-3559C132.08,-3559 152.53,-3559 171.66,-3559"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="172.09,-3561.1 178.09,-3559 172.09,-3556.9 172.09,-3561.1"/>
 </g>
 <!-- red_sub_gc -->
-<g id="node115" class="node">
+<g id="node120" class="node">
 <title>red_sub_gc</title>
-<g id="a_node115"><a xlink:title="red_sub_gc theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
+<g id="a_node120"><a xlink:title="red_sub_gc theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
 <ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-70" rx="36.25" ry="18"/>
 <text text-anchor="middle" x="239.88" y="-67.8" font-family="Inter" font-size="9.00" fill="#222222">red_sub_gc</text>
 </a>
 </g>
 </g>
 <!-- red_sub_gc&#45;&gt;full_comp_aux_sub -->
-<g id="edge78" class="edge">
+<g id="edge80" class="edge">
 <title>red_sub_gc&#45;&gt;full_comp_aux_sub</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M272.17,-78.4C284.24,-83.03 297.29,-89.94 306.27,-100 347.09,-145.71 308.19,-185.53 349.27,-231 353.05,-235.18 357.62,-238.72 362.52,-241.71"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="361.69,-243.65 367.95,-244.75 363.74,-239.99 361.69,-243.65"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M271.8,-78.71C283.28,-82.83 296,-88.52 306.27,-96 330.52,-113.65 330.02,-125 349.27,-148 362.47,-163.76 377.46,-181.45 388.96,-194.97"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="387.54,-196.54 393.02,-199.75 390.74,-193.82 387.54,-196.54"/>
 </g>
 <!-- red_gc_to_red_sub -->
-<g id="node127" class="node">
+<g id="node132" class="node">
 <title>red_gc_to_red_sub</title>
-<g id="a_node127"><a xlink:title="red_gc_to_red_sub theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
+<g id="a_node132"><a xlink:title="red_gc_to_red_sub theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
 <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">red_gc_to_red_sub</text>
 </a>
 </g>
 </g>
 <!-- red_sub_gc&#45;&gt;red_gc_to_red_sub -->
-<g id="edge87" class="edge">
+<g id="edge89" class="edge">
 <title>red_sub_gc&#45;&gt;red_gc_to_red_sub</title>
 <path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M276.26,-70C297.34,-70 324.63,-70 348.87,-70"/>
 <polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="348.96,-72.1 354.96,-70 348.96,-67.9 348.96,-72.1"/>
 </g>
 <!-- red_sub_r -->
-<g id="node116" class="node">
+<g id="node121" class="node">
 <title>red_sub_r</title>
-<g id="a_node116"><a xlink:title="red_sub_r theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-156" rx="32.82" ry="18"/>
-<text text-anchor="middle" x="239.88" y="-153.8" font-family="Inter" font-size="9.00" fill="#222222">red_sub_r</text>
+<g id="a_node121"><a xlink:title="red_sub_r theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-174" rx="32.82" ry="18"/>
+<text text-anchor="middle" x="239.88" y="-171.8" font-family="Inter" font-size="9.00" fill="#222222">red_sub_r</text>
 </a>
 </g>
 </g>
 <!-- red_sub_r&#45;&gt;full_comp_aux_sub -->
-<g id="edge79" class="edge">
+<g id="edge81" class="edge">
 <title>red_sub_r&#45;&gt;full_comp_aux_sub</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M269.38,-164.05C281.42,-168.25 295.19,-174.18 306.27,-182 329.95,-198.7 325.94,-213.83 349.27,-231 354.41,-234.78 360.18,-238.17 366.05,-241.16"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="365.14,-243.05 371.45,-243.79 366.98,-239.28 365.14,-243.05"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M269.94,-181.49C294.44,-187.8 330.01,-196.97 358.87,-204.41"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="358.59,-206.5 364.92,-205.97 359.64,-202.44 358.59,-206.5"/>
 </g>
 <!-- occurs_zfill -->
-<g id="node117" class="node">
+<g id="node122" class="node">
 <title>occurs_zfill</title>
-<g id="a_node117"><a xlink:title="occurs_zfill theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-3493" rx="37.56" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-3490.8" font-family="Inter" font-size="9.00" fill="#222222">occurs_zfill</text>
+<g id="a_node122"><a xlink:title="occurs_zfill theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-3611" rx="37.56" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-3608.8" font-family="Inter" font-size="9.00" fill="#222222">occurs_zfill</text>
 </a>
 </g>
 </g>
 <!-- zfill_occurs0 -->
-<g id="node118" class="node">
+<g id="node123" class="node">
 <title>zfill_occurs0</title>
-<g id="a_node118"><a xlink:title="zfill_occurs0 theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-3493" rx="40.98" ry="18"/>
-<text text-anchor="middle" x="239.88" y="-3490.8" font-family="Inter" font-size="9.00" fill="#222222">zfill_occurs0</text>
+<g id="a_node123"><a xlink:title="zfill_occurs0 theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-3611" rx="40.98" ry="18"/>
+<text text-anchor="middle" x="239.88" y="-3608.8" font-family="Inter" font-size="9.00" fill="#222222">zfill_occurs0</text>
 </a>
 </g>
 </g>
 <!-- occurs_zfill&#45;&gt;zfill_occurs0 -->
-<g id="edge71" class="edge">
+<g id="edge73" class="edge">
 <title>occurs_zfill&#45;&gt;zfill_occurs0</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M102.85,-3493C128.98,-3493 164.34,-3493 192.45,-3493"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="192.7,-3495.1 198.7,-3493 192.7,-3490.9 192.7,-3495.1"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M102.85,-3611C128.98,-3611 164.34,-3611 192.45,-3611"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="192.7,-3613.1 198.7,-3611 192.7,-3608.9 192.7,-3613.1"/>
 </g>
 <!-- R_Gc_disjoint -->
-<g id="node119" class="node">
+<g id="node124" class="node">
 <title>R_Gc_disjoint</title>
-<g id="a_node119"><a xlink:title="R_Gc_disjoint theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-3493" rx="41.64" ry="18"/>
-<text text-anchor="middle" x="408.74" y="-3490.8" font-family="Inter" font-size="9.00" fill="#222222">R_Gc_disjoint</text>
+<g id="a_node124"><a xlink:title="R_Gc_disjoint theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-3611" rx="41.64" ry="18"/>
+<text text-anchor="middle" x="408.74" y="-3608.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="edge72" class="edge">
+<g id="edge74" class="edge">
 <title>zfill_occurs0&#45;&gt;R_Gc_disjoint</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M281.27,-3493C305.28,-3493 335.83,-3493 360.89,-3493"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="361.14,-3495.1 367.14,-3493 361.14,-3490.9 361.14,-3495.1"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M281.27,-3611C305.28,-3611 335.83,-3611 360.89,-3611"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="361.14,-3613.1 367.14,-3611 361.14,-3608.9 361.14,-3613.1"/>
 </g>
 <!-- plus_red_sub_full_comp -->
-<g id="node122" class="node">
+<g id="node127" class="node">
 <title>plus_red_sub_full_comp</title>
-<g id="a_node122"><a xlink:title="plus_red_sub_full_comp theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="577.6" cy="-255" rx="66.29" ry="18"/>
-<text text-anchor="middle" x="577.6" y="-252.8" font-family="Inter" font-size="9.00" fill="#222222">plus_red_sub_full_comp</text>
+<g id="a_node127"><a xlink:title="plus_red_sub_full_comp theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="578.76" cy="-197" rx="66.29" ry="18"/>
+<text text-anchor="middle" x="578.76" y="-194.8" font-family="Inter" font-size="9.00" fill="#222222">plus_red_sub_full_comp</text>
 </a>
 </g>
 </g>
 <!-- full_comp_aux_sub&#45;&gt;plus_red_sub_full_comp -->
-<g id="edge82" class="edge">
+<g id="edge84" class="edge">
 <title>full_comp_aux_sub&#45;&gt;plus_red_sub_full_comp</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M463.91,-256.35C476.95,-256.19 491.08,-256.03 504.79,-255.86"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="505.07,-257.96 511.05,-255.79 505.02,-253.76 505.07,-257.96"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M460.61,-210.95C476.61,-209.04 494.52,-206.91 511.42,-204.9"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="511.89,-206.95 517.6,-204.16 511.4,-202.78 511.89,-206.95"/>
 </g>
 <!-- plus_red_sub_full_comp&#45;&gt;star_red_sub_full_comp -->
-<g id="edge84" class="edge">
+<g id="edge86" class="edge">
 <title>plus_red_sub_full_comp&#45;&gt;star_red_sub_full_comp</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M636.28,-263.66C653.02,-266.17 671.39,-268.93 688.46,-271.49"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="688.44,-273.61 694.68,-272.42 689.06,-269.46 688.44,-273.61"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M637.33,-205.59C654.38,-208.13 673.15,-210.93 690.56,-213.52"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="690.66,-215.66 696.9,-214.47 691.28,-211.51 690.66,-215.66"/>
 </g>
 <!-- es_count_plug_mono -->
-<g id="node124" class="node">
+<g id="node129" class="node">
 <title>es_count_plug_mono</title>
-<g id="a_node124"><a xlink:title="es_count_plug_mono theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-3545" rx="60.74" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-3542.8" font-family="Inter" font-size="9.00" fill="#222222">es_count_plug_mono</text>
+<g id="a_node129"><a xlink:title="es_count_plug_mono theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-3663" rx="60.74" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-3660.8" font-family="Inter" font-size="9.00" fill="#222222">es_count_plug_mono</text>
 </a>
 </g>
 </g>
 <!-- red_gc_measure -->
-<g id="node125" class="node">
+<g id="node130" class="node">
 <title>red_gc_measure</title>
-<g id="a_node125"><a xlink:title="red_gc_measure theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-3545" rx="49.8" ry="18"/>
-<text text-anchor="middle" x="239.88" y="-3542.8" font-family="Inter" font-size="9.00" fill="#222222">red_gc_measure</text>
+<g id="a_node130"><a xlink:title="red_gc_measure theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-3663" rx="49.8" ry="18"/>
+<text text-anchor="middle" x="239.88" y="-3660.8" font-family="Inter" font-size="9.00" fill="#222222">red_gc_measure</text>
 </a>
 </g>
 </g>
 <!-- es_count_plug_mono&#45;&gt;red_gc_measure -->
-<g id="edge85" class="edge">
+<g id="edge87" class="edge">
 <title>es_count_plug_mono&#45;&gt;red_gc_measure</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M126.14,-3545C144.95,-3545 165.61,-3545 184.05,-3545"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="184.22,-3547.1 190.22,-3545 184.22,-3542.9 184.22,-3547.1"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M126.14,-3663C144.95,-3663 165.61,-3663 184.05,-3663"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="184.22,-3665.1 190.22,-3663 184.22,-3660.9 184.22,-3665.1"/>
 </g>
 <!-- red_gc_terminates -->
-<g id="node126" class="node">
+<g id="node131" class="node">
 <title>red_gc_terminates</title>
-<g id="a_node126"><a xlink:title="red_gc_terminates theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-3545" rx="54.04" ry="18"/>
-<text text-anchor="middle" x="408.74" y="-3542.8" font-family="Inter" font-size="9.00" fill="#222222">red_gc_terminates</text>
+<g id="a_node131"><a xlink:title="red_gc_terminates theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-3663" rx="54.04" ry="18"/>
+<text text-anchor="middle" x="408.74" y="-3660.8" font-family="Inter" font-size="9.00" fill="#222222">red_gc_terminates</text>
 </a>
 </g>
 </g>
 <!-- red_gc_measure&#45;&gt;red_gc_terminates -->
-<g id="edge86" class="edge">
+<g id="edge88" class="edge">
 <title>red_gc_measure&#45;&gt;red_gc_terminates</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M289.59,-3545C307.82,-3545 328.75,-3545 347.88,-3545"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="348.29,-3547.1 354.29,-3545 348.29,-3542.9 348.29,-3547.1"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M289.59,-3663C307.82,-3663 328.75,-3663 347.88,-3663"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="348.29,-3665.1 354.29,-3663 348.29,-3660.9 348.29,-3665.1"/>
 </g>
 </g>
 </svg>
diff --git a/graphs/theorems.json b/graphs/theorems.json
index 1ed9d7a..672b9e8 100644
--- a/graphs/theorems.json
+++ b/graphs/theorems.json
@@ -467,6 +467,39 @@
       "file": "theory/Metaterm.v",
       "depends": []
     },
+    {
+      "id": "Plus_mred_of_Plus_red1",
+      "label": "Plus_mred_of_Plus_red1",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M0",
+      "section": "",
+      "file": "theory/Metaterm.v",
+      "depends": []
+    },
+    {
+      "id": "mred_full_comp_pure",
+      "label": "mred_full_comp_pure",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M0",
+      "section": "",
+      "file": "theory/Metaterm.v",
+      "depends": [
+        "Plus_mred_of_Plus_red1",
+        "lemma_2_2_full_comp"
+      ]
+    },
+    {
+      "id": "mred_plus_one",
+      "label": "mred_plus_one",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M0",
+      "section": "",
+      "file": "theory/Metaterm.v",
+      "depends": []
+    },
     {
       "id": "Plus_red1_context",
       "label": "Plus_red1_context",
@@ -706,6 +739,26 @@
       "file": "theory/NamedMeta.v",
       "depends": []
     },
+    {
+      "id": "Es_ctx_any",
+      "label": "Es_ctx_any",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M0",
+      "section": "",
+      "file": "theory/NamedMeta.v",
+      "depends": []
+    },
+    {
+      "id": "nred_R_intro",
+      "label": "nred_R_intro",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M0",
+      "section": "",
+      "file": "theory/NamedMeta.v",
+      "depends": []
+    },
     {
       "id": "Es_refl_any",
       "label": "Es_refl_any",
diff --git a/theory/NamedMeta.v b/theory/NamedMeta.v
index 25640d4..a267974 100644
--- a/theory/NamedMeta.v
+++ b/theory/NamedMeta.v
@@ -70,7 +70,21 @@ Inductive Es : ntrm -> ntrm -> Prop :=
 | Es_trans : forall t u v, Es t u -> Es u v -> Es t v
 | Es_C : forall t x u y v,
     y <> x -> ~ In y (nfv u) -> ~ In x (nfv v) ->
-    Es (NESub (NESub t x u) y v) (NESub (NESub t y v) x u).
+    Es (NESub (NESub t x u) y v) (NESub (NESub t y v) x u)
+| Es_ctx : forall C t t', Es t t' -> Es (nplug C t) (nplug C t').
+
+Fixpoint cbinders (C : nctx) : list atom :=
+  match C with
+  | nHole => []
+  | nAppL C1 _ => cbinders C1
+  | nAppR _ C1 => cbinders C1
+  | nLam x C1 => x :: cbinders C1
+  | nESubL C1 _ _ => cbinders C1
+  | nESubR _ _ C1 => cbinders C1
+  end.
+
+Definition cavoid (C : nctx) (phi : list atom) : bool :=
+  forallb (fun y => negb (existsb (Nat.eqb y) phi)) (cbinders C).
 
 Inductive nred : ntrm -> ntrm -> Prop :=
 | nred_B : forall t x u, nred (NApp (NLam x t) u) (NESub t x u)
@@ -82,6 +96,11 @@ Inductive nred : ntrm -> ntrm -> Prop :=
     is_subst_chain C = false ->
     nred (NESub (nplug C (NMVar X d)) x u)
          (NESub (nplug C (NESub (NMVar X d) x u)) x u)
+| nred_R : forall C x u phi,
+    In x phi ->
+    (forall y, In y (nfv u) -> In y phi) ->
+    cavoid C phi = true ->
+    nred (NESub (nplug C (NVar x)) x u) (NESub (nplug C u) x u)
 | nred_ctx : forall C t t', nred t t' -> nred (nplug C t) (nplug C t').
 
 Lemma eqC_in_Es : forall t x u y v,
@@ -89,6 +108,20 @@ Lemma eqC_in_Es : forall t x u y v,
   Es (NESub (NESub t x u) y v) (NESub (NESub t y v) x u).
 Proof. intros. apply Es_C; assumption. Qed.
 
+Lemma Es_ctx_any : forall C t t', Es t t' -> Es (nplug C t) (nplug C t').
+Proof. intros. apply Es_ctx. exact H. Qed.
+
+Lemma nred_R_intro : forall C x u phi,
+  In x phi -> (forall y, In y (nfv u) -> In y phi) -> cavoid C phi = true ->
+  nred (NESub (nplug C (NVar x)) x u) (NESub (nplug C u) x u).
+Proof.
+  intros C x u phi Hx Hu Hc.
+  apply nred_R with (phi := phi).
+  - exact Hx.
+  - exact Hu.
+  - exact Hc.
+Qed.
+
 Lemma Es_refl_any : forall t, Es t t.
 Proof. intros. apply Es_refl. Qed.
 
@@ -100,6 +133,8 @@ Proof. intros. apply Es_trans with (u := u); assumption. Qed.
 
 Print Assumptions isubst_meta_in.
 Print Assumptions isubst_meta_notin.
+Print Assumptions Es_ctx_any.
+Print Assumptions nred_R_intro.
 Print Assumptions eqC_in_Es.
 Print Assumptions Es_refl_any.
 Print Assumptions Es_sym_any.