diff --git a/graphs/dependency.dot b/graphs/dependency.dot
index 4dbe0fb..9fb35b0 100644
--- a/graphs/dependency.dot
+++ b/graphs/dependency.dot
@@ -85,6 +85,9 @@ digraph theorem_deps {
   nred_core_fv [label="nred_core_fv", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="nred_core_fv theory/NamedMeta.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
   nplug_esub_fv [label="nplug_esub_fv", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="nplug_esub_fv theory/NamedMeta.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
   nred_fv [label="nred_fv", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="nred_fv theory/NamedMeta.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  in_filter_neq_iff [label="in_filter_neq_iff", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="in_filter_neq_iff theory/NamedMeta.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  Es_fv_both [label="Es_fv_both", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="Es_fv_both theory/NamedMeta.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  Es_fv [label="Es_fv", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="Es_fv theory/NamedMeta.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
   par_red1_iff [label="par_red1_iff", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="par_red1_iff theory/Parallel.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
   red1_in_par [label="red1_in_par", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="red1_in_par theory/Parallel.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
   par_context [label="par_context", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="par_context theory/Parallel.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
@@ -203,6 +206,9 @@ digraph theorem_deps {
   nplug_esub_fv -> nred_fv;
   nplug_fv_mono -> nred_fv;
   nplug_fv_upper -> nred_fv;
+  in_filter_neq_iff -> Es_fv_both;
+  nplug_fv_mono -> Es_fv_both;
+  Es_fv_both -> Es_fv;
   par_red1_iff -> par_to_red1_or_eq;
   par_red1_iff -> red1_or_eq_to_par;
   has_red_spec -> check_term_true;
diff --git a/graphs/dependency.png b/graphs/dependency.png
index 89c8c95..c465ece 100644
Binary files a/graphs/dependency.png and b/graphs/dependency.png differ
diff --git a/graphs/dependency.svg b/graphs/dependency.svg
index 466e642..c473e9a 100644
--- a/graphs/dependency.svg
+++ b/graphs/dependency.svg
@@ -4,19 +4,19 @@
 <!-- Generated by graphviz version 2.42.4 (0)
  -->
 <!-- Title: theorem_deps Pages: 1 -->
-<svg width="1296pt" height="3950pt"
- viewBox="0.00 0.00 1296.27 3950.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 3946)">
+<svg width="1296pt" height="3959pt"
+ viewBox="0.00 0.00 1296.27 3959.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 3955)">
 <title>theorem_deps</title>
-<polygon fill="white" stroke="transparent" points="-4,4 -4,-3946 1292.27,-3946 1292.27,4 -4,4"/>
-<text text-anchor="start" x="407.63" y="-3929.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="-3919.8" font-family="Inter" font-size="9.00" fill="#38761d">proved</text>
-<text text-anchor="start" x="601.13" y="-3919.8" font-family="Inter" font-size="9.00"> &#160;&#160;</text>
-<text text-anchor="start" x="608.13" y="-3919.8" font-family="Inter" font-size="9.00" fill="#b45f06">stated</text>
-<text text-anchor="start" x="635.13" y="-3919.8" font-family="Inter" font-size="9.00"> &#160;&#160;</text>
-<text text-anchor="start" x="642.13" y="-3919.8" font-family="Inter" font-size="9.00" fill="#777777">planned</text>
-<text text-anchor="start" x="676.13" y="-3919.8" font-family="Inter" font-size="9.00"> &#160;&#160;</text>
-<text text-anchor="start" x="683.13" y="-3919.8" font-family="Inter" font-size="9.00" fill="#cc0000">blocked</text>
+<polygon fill="white" stroke="transparent" points="-4,4 -4,-3955 1292.27,-3955 1292.27,4 -4,4"/>
+<text text-anchor="start" x="407.63" y="-3938.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="-3928.8" font-family="Inter" font-size="9.00" fill="#38761d">proved</text>
+<text text-anchor="start" x="601.13" y="-3928.8" font-family="Inter" font-size="9.00"> &#160;&#160;</text>
+<text text-anchor="start" x="608.13" y="-3928.8" font-family="Inter" font-size="9.00" fill="#b45f06">stated</text>
+<text text-anchor="start" x="635.13" y="-3928.8" font-family="Inter" font-size="9.00"> &#160;&#160;</text>
+<text text-anchor="start" x="642.13" y="-3928.8" font-family="Inter" font-size="9.00" fill="#777777">planned</text>
+<text text-anchor="start" x="676.13" y="-3928.8" font-family="Inter" font-size="9.00"> &#160;&#160;</text>
+<text text-anchor="start" x="683.13" y="-3928.8" font-family="Inter" font-size="9.00" fill="#cc0000">blocked</text>
 <!-- fvs_lift -->
 <g id="node1" class="node">
 <title>fvs_lift</title>
@@ -138,8 +138,8 @@
 <g id="node6" class="node">
 <title>open_rec_occurs_false</title>
 <g id="a_node6"><a xlink:title="open_rec_occurs_false theory/Binding.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-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>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-239" rx="65.48" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-236.8" font-family="Inter" font-size="9.00" fill="#222222">open_rec_occurs_false</text>
 </a>
 </g>
 </g>
@@ -155,8 +155,8 @@
 <!-- open_rec_occurs_false&#45;&gt;open_rec_zplug_lift -->
 <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="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"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M125.17,-246.17C143.16,-248.36 162.92,-250.76 180.85,-252.94"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="180.65,-255.03 186.86,-253.67 181.15,-250.86 180.65,-255.03"/>
 </g>
 <!-- full_comp_aux -->
 <g id="node54" class="node">
@@ -170,38 +170,38 @@
 <!-- open_rec_occurs_false&#45;&gt;full_comp_aux -->
 <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="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"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M83.93,-256.56C111.5,-283.74 162.71,-333.39 173.48,-338 233.83,-363.85 311,-363.11 359.92,-359"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="360.25,-361.08 366.04,-358.46 359.87,-356.9 360.25,-361.08"/>
 </g>
 <!-- subst_notin -->
-<g id="node119" class="node">
+<g id="node122" class="node">
 <title>subst_notin</title>
-<g id="a_node119"><a xlink:title="subst_notin theory/Substitution.v https://arxiv.org/html/2312.13270v1">
+<g id="a_node122"><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="edge83" class="edge">
+<g id="edge86" class="edge">
 <title>open_rec_occurs_false&#45;&gt;subst_notin</title>
-<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"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M71.52,-221.02C83.51,-183.14 116.28,-94.5 173.48,-44 181.14,-37.24 190.78,-32.12 200.28,-28.29"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="201.29,-30.15 206.16,-26.07 199.81,-26.23 201.29,-30.15"/>
 </g>
 <!-- full_comp_aux_sub -->
-<g id="node133" class="node">
+<g id="node136" class="node">
 <title>full_comp_aux_sub</title>
-<g id="a_node133"><a xlink:title="full_comp_aux_sub theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
+<g id="a_node136"><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="edge93" class="edge">
+<g id="edge96" class="edge">
 <title>open_rec_occurs_false&#45;&gt;full_comp_aux_sub</title>
-<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"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M128.88,-234.96C191.52,-230.93 287.14,-224.77 348.54,-220.81"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="348.89,-222.9 354.75,-220.41 348.62,-218.7 348.89,-222.9"/>
 </g>
 <!-- close_rec_notin -->
 <g id="node7" class="node">
@@ -213,7 +213,7 @@
 </g>
 </g>
 <!-- close_rec_notin&#45;&gt;subst_notin -->
-<g id="edge82" class="edge">
+<g id="edge85" 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"/>
@@ -264,16 +264,16 @@
 <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="node120" class="node">
+<g id="node123" class="node">
 <title>subst_lc_self</title>
-<g id="a_node120"><a xlink:title="subst_lc_self theory/Substitution.v https://arxiv.org/html/2312.13270v1">
+<g id="a_node123"><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="edge84" class="edge">
+<g id="edge87" class="edge">
 <title>subst_fvar_self&#45;&gt;subst_lc_self</title>
 <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"/>
@@ -288,16 +288,16 @@
 </g>
 </g>
 <!-- subst_other -->
-<g id="node121" class="node">
+<g id="node124" class="node">
 <title>subst_other</title>
-<g id="a_node121"><a xlink:title="subst_other theory/Substitution.v https://arxiv.org/html/2312.13270v1">
+<g id="a_node124"><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="edge85" class="edge">
+<g id="edge88" class="edge">
 <title>subst_fvar_other&#45;&gt;subst_other</title>
 <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"/>
@@ -330,16 +330,16 @@
 </g>
 </g>
 <!-- star_red_sub_full_comp -->
-<g id="node135" class="node">
+<g id="node138" class="node">
 <title>star_red_sub_full_comp</title>
-<g id="a_node135"><a xlink:title="star_red_sub_full_comp theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
+<g id="a_node138"><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="edge100" class="edge">
+<g id="edge103" class="edge">
 <title>Plus_to_Star&#45;&gt;star_red_sub_full_comp</title>
 <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"/>
@@ -693,7 +693,7 @@
 <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="edge91" class="edge">
+<g id="edge94" class="edge">
 <title>occurs_count_zero&#45;&gt;full_comp_aux_sub</title>
 <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"/>
@@ -726,22 +726,22 @@
 <g id="node50" class="node">
 <title>occurs_lift_self</title>
 <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>
+<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>
 </a>
 </g>
 </g>
 <!-- occurs_lift_self&#45;&gt;occurs_count_zfill_plug -->
 <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="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"/>
+<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"/>
 </g>
 <!-- occurs_lift_self&#45;&gt;open_rec_zplug_lift -->
 <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="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"/>
+<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"/>
 </g>
 <!-- zdecs_nonempty -->
 <g id="node51" class="node">
@@ -759,7 +759,7 @@
 <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="edge97" class="edge">
+<g id="edge100" class="edge">
 <title>zdecs_nonempty&#45;&gt;full_comp_aux_sub</title>
 <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"/>
@@ -771,7 +771,7 @@
 <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="edge92" class="edge">
+<g id="edge95" class="edge">
 <title>occurs_count_zfill_plug&#45;&gt;full_comp_aux_sub</title>
 <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"/>
@@ -783,7 +783,7 @@
 <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="edge94" class="edge">
+<g id="edge97" class="edge">
 <title>open_rec_zplug_lift&#45;&gt;full_comp_aux_sub</title>
 <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"/>
@@ -876,31 +876,31 @@
 <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="node90" class="node">
+<g id="node93" class="node">
 <title>gen_fv_preserved</title>
-<g id="a_node90"><a xlink:title="gen_fv_preserved theory/Random.v https://arxiv.org/html/2312.13270v1">
+<g id="a_node93"><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="edge61" class="edge">
+<g id="edge64" class="edge">
 <title>lemma_2_1_fv_preserved&#45;&gt;gen_fv_preserved</title>
 <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="node143" class="node">
+<g id="node146" class="node">
 <title>corpus_fv_preserved</title>
-<g id="a_node143"><a xlink:title="corpus_fv_preserved theory/Tests.v https://arxiv.org/html/2312.13270v1">
+<g id="a_node146"><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="edge108" class="edge">
+<g id="edge111" class="edge">
 <title>lemma_2_1_fv_preserved&#45;&gt;corpus_fv_preserved</title>
 <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"/>
@@ -1008,61 +1008,61 @@
 <g id="node74" class="node">
 <title>nplug_fv_mono</title>
 <g id="a_node74"><a xlink:title="nplug_fv_mono theory/NamedMeta.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-2675" rx="46.38" ry="18"/>
-<text text-anchor="middle" x="239.88" y="-2672.8" font-family="Inter" font-size="9.00" fill="#222222">nplug_fv_mono</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-2684" rx="46.38" ry="18"/>
+<text text-anchor="middle" x="239.88" y="-2681.8" font-family="Inter" font-size="9.00" fill="#222222">nplug_fv_mono</text>
 </a>
 </g>
 </g>
 <!-- in_filter_neq&#45;&gt;nplug_fv_mono -->
 <g id="edge40" class="edge">
 <title>in_filter_neq&#45;&gt;nplug_fv_mono</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M98.71,-2717.22C126.46,-2708.86 166.56,-2696.78 196.77,-2687.68"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="197.53,-2689.65 202.67,-2685.91 196.32,-2685.63 197.53,-2689.65"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M100.35,-2718.5C127.32,-2711.79 165.18,-2702.36 194.51,-2695.05"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="195.32,-2697.01 200.63,-2693.53 194.3,-2692.94 195.32,-2697.01"/>
 </g>
 <!-- nplug_fv_upper -->
 <g id="node75" class="node">
 <title>nplug_fv_upper</title>
 <g id="a_node75"><a xlink:title="nplug_fv_upper theory/NamedMeta.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-2727" rx="46.38" ry="18"/>
-<text text-anchor="middle" x="239.88" y="-2724.8" font-family="Inter" font-size="9.00" fill="#222222">nplug_fv_upper</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-2770" rx="46.38" ry="18"/>
+<text text-anchor="middle" x="239.88" y="-2767.8" font-family="Inter" font-size="9.00" fill="#222222">nplug_fv_upper</text>
 </a>
 </g>
 </g>
 <!-- in_filter_neq&#45;&gt;nplug_fv_upper -->
 <g id="edge42" class="edge">
 <title>in_filter_neq&#45;&gt;nplug_fv_upper</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M104.55,-2727C128.92,-2727 160.78,-2727 187.35,-2727"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="187.63,-2729.1 193.63,-2727 187.63,-2724.9 187.63,-2729.1"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M100.35,-2735.5C127.32,-2742.21 165.18,-2751.64 194.51,-2758.95"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="194.3,-2761.06 200.63,-2760.47 195.32,-2756.99 194.3,-2761.06"/>
 </g>
 <!-- nred_core_fv -->
 <g id="node76" class="node">
 <title>nred_core_fv</title>
 <g id="a_node76"><a xlink:title="nred_core_fv theory/NamedMeta.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-2697" rx="40.33" ry="18"/>
-<text text-anchor="middle" x="408.74" y="-2694.8" font-family="Inter" font-size="9.00" fill="#222222">nred_core_fv</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-2701" rx="40.33" ry="18"/>
+<text text-anchor="middle" x="408.74" y="-2698.8" font-family="Inter" font-size="9.00" fill="#222222">nred_core_fv</text>
 </a>
 </g>
 </g>
 <!-- in_filter_neq&#45;&gt;nred_core_fv -->
 <g id="edge44" class="edge">
 <title>in_filter_neq&#45;&gt;nred_core_fv</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M98.58,-2717.48C109.33,-2713.41 120.97,-2707.97 130.48,-2701 154.67,-2683.28 146.35,-2661.77 173.48,-2649 242.42,-2616.55 332.92,-2655.3 378.63,-2679.84"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="377.7,-2681.73 383.98,-2682.76 379.71,-2678.04 377.7,-2681.73"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M98.21,-2716.95C108.93,-2712.85 120.65,-2707.51 130.48,-2701 153.01,-2686.08 148.51,-2668.34 173.48,-2658 242.35,-2629.47 330.4,-2662.45 376.46,-2684.46"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="375.82,-2686.48 382.14,-2687.21 377.66,-2682.7 375.82,-2686.48"/>
 </g>
 <!-- nplug_esub_fv -->
 <g id="node77" class="node">
 <title>nplug_esub_fv</title>
 <g id="a_node77"><a xlink:title="nplug_esub_fv theory/NamedMeta.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-2813" rx="43.76" ry="18"/>
-<text text-anchor="middle" x="239.88" y="-2810.8" font-family="Inter" font-size="9.00" fill="#222222">nplug_esub_fv</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-2822" rx="43.76" ry="18"/>
+<text text-anchor="middle" x="239.88" y="-2819.8" font-family="Inter" font-size="9.00" fill="#222222">nplug_esub_fv</text>
 </a>
 </g>
 </g>
 <!-- in_filter_neq&#45;&gt;nplug_esub_fv -->
 <g id="edge48" class="edge">
 <title>in_filter_neq&#45;&gt;nplug_esub_fv</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M91.62,-2740.72C113.23,-2752.29 145.19,-2769.14 173.48,-2783 183.23,-2787.78 193.9,-2792.77 203.74,-2797.28"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="203.1,-2799.3 209.43,-2799.88 204.84,-2795.48 203.1,-2799.3"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M87.28,-2742.28C108.39,-2757.18 142.18,-2779.9 173.48,-2796 181.95,-2800.36 191.32,-2804.47 200.26,-2808.08"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="199.71,-2810.12 206.06,-2810.38 201.26,-2806.22 199.71,-2810.12"/>
 </g>
 <!-- nred_fv -->
 <g id="node78" class="node">
@@ -1076,173 +1076,218 @@
 <!-- in_filter_neq&#45;&gt;nred_fv -->
 <g id="edge50" class="edge">
 <title>in_filter_neq&#45;&gt;nred_fv</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M98.81,-2736.38C119.92,-2742.1 148.12,-2749.03 173.48,-2753 245.05,-2764.19 330.09,-2768.04 375.45,-2769.34"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="375.53,-2771.45 381.58,-2769.51 375.64,-2767.25 375.53,-2771.45"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M104.73,-2727.6C152.35,-2728.82 235.76,-2732.56 306.27,-2744 330.67,-2747.96 357.77,-2755.04 377.82,-2760.82"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="377.46,-2762.9 383.81,-2762.56 378.63,-2758.87 377.46,-2762.9"/>
 </g>
 <!-- filter_neq_in -->
 <g id="node73" class="node">
 <title>filter_neq_in</title>
 <g id="a_node73"><a xlink:title="filter_neq_in theory/NamedMeta.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-2813" rx="39.02" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-2810.8" font-family="Inter" font-size="9.00" fill="#222222">filter_neq_in</text>
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-2822" rx="39.02" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-2819.8" font-family="Inter" font-size="9.00" fill="#222222">filter_neq_in</text>
 </a>
 </g>
 </g>
 <!-- filter_neq_in&#45;&gt;nplug_fv_mono -->
 <g id="edge39" class="edge">
 <title>filter_neq_in&#45;&gt;nplug_fv_mono</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M84.56,-2797.04C97.74,-2785.28 115.73,-2768.67 130.48,-2753 151.04,-2731.16 149.23,-2718.65 173.48,-2701 180.54,-2695.86 188.76,-2691.56 196.94,-2688.04"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="197.83,-2689.94 202.58,-2685.72 196.23,-2686.06 197.83,-2689.94"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M85.71,-2806.44C117.14,-2781.31 179.05,-2731.82 213.76,-2704.07"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="215.31,-2705.53 218.68,-2700.14 212.68,-2702.25 215.31,-2705.53"/>
 </g>
 <!-- filter_neq_in&#45;&gt;nplug_fv_upper -->
 <g id="edge41" class="edge">
 <title>filter_neq_in&#45;&gt;nplug_fv_upper</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M92.46,-2799.94C122.6,-2784.92 172.14,-2760.24 205.13,-2743.81"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="206.25,-2745.6 210.69,-2741.04 204.38,-2741.84 206.25,-2745.6"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M98.71,-2812.22C126.46,-2803.86 166.56,-2791.78 196.77,-2782.68"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="197.53,-2784.65 202.67,-2780.91 196.32,-2780.63 197.53,-2784.65"/>
 </g>
 <!-- filter_neq_in&#45;&gt;nred_core_fv -->
 <g id="edge43" class="edge">
 <title>filter_neq_in&#45;&gt;nred_core_fv</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M92.9,-2826.07C140.07,-2847.12 239.52,-2882.06 306.27,-2839 345.22,-2813.88 320.88,-2780.63 349.27,-2744 357.71,-2733.12 369.14,-2723.21 379.66,-2715.33"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="381.13,-2716.86 384.74,-2711.62 378.65,-2713.46 381.13,-2716.86"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M92.68,-2835.12C139.92,-2856.5 240.07,-2892.27 306.27,-2848 347.85,-2820.2 318.43,-2783.38 349.27,-2744 357.01,-2734.12 367.58,-2725.41 377.61,-2718.47"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="378.97,-2720.08 382.79,-2715 376.63,-2716.59 378.97,-2720.08"/>
 </g>
 <!-- filter_neq_in&#45;&gt;nplug_esub_fv -->
 <g id="edge47" class="edge">
 <title>filter_neq_in&#45;&gt;nplug_esub_fv</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M104.55,-2813C129.67,-2813 162.75,-2813 189.79,-2813"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="189.81,-2815.1 195.81,-2813 189.81,-2810.9 189.81,-2815.1"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M104.55,-2822C129.67,-2822 162.75,-2822 189.79,-2822"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="189.81,-2824.1 195.81,-2822 189.81,-2819.9 189.81,-2824.1"/>
 </g>
 <!-- filter_neq_in&#45;&gt;nred_fv -->
 <g id="edge49" class="edge">
 <title>filter_neq_in&#45;&gt;nred_fv</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M87.58,-2828.12C108.38,-2841.86 141.46,-2861.14 173.48,-2869 230.8,-2883.06 251.61,-2891.25 306.27,-2869 344.58,-2853.41 376.32,-2815.63 393.6,-2791.51"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="395.33,-2792.7 397.07,-2786.58 391.9,-2790.28 395.33,-2792.7"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M87.58,-2837.12C108.38,-2850.86 141.46,-2870.14 173.48,-2878 230.8,-2892.06 252.1,-2901.43 306.27,-2878 346.61,-2860.55 378.3,-2818.29 394.92,-2792.11"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="396.85,-2792.98 398.23,-2786.78 393.28,-2790.76 396.85,-2792.98"/>
 </g>
 <!-- nplug_fv_mono&#45;&gt;nred_core_fv -->
 <g id="edge45" class="edge">
 <title>nplug_fv_mono&#45;&gt;nred_core_fv</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M283.85,-2680.67C308.33,-2683.89 338.94,-2687.93 363.61,-2691.18"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="363.52,-2693.29 369.75,-2691.99 364.07,-2689.12 363.52,-2693.29"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M284.72,-2688.47C308.84,-2690.92 338.71,-2693.97 362.98,-2696.44"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="362.84,-2698.54 369.02,-2697.06 363.27,-2694.36 362.84,-2698.54"/>
 </g>
 <!-- nplug_fv_mono&#45;&gt;nred_fv -->
 <g id="edge52" class="edge">
 <title>nplug_fv_mono&#45;&gt;nred_fv</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M274.78,-2686.85C285.1,-2690.89 296.34,-2695.73 306.27,-2701 335.07,-2716.28 365.7,-2737.95 385.67,-2752.91"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="384.46,-2754.62 390.52,-2756.56 386.99,-2751.27 384.46,-2754.62"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M271.38,-2697.43C282.45,-2702.45 295.01,-2708.32 306.27,-2714 332.66,-2727.31 362.17,-2743.78 382.53,-2755.4"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="381.51,-2757.24 387.76,-2758.4 383.6,-2753.6 381.51,-2757.24"/>
+</g>
+<!-- Es_fv_both -->
+<g id="node80" class="node">
+<title>Es_fv_both</title>
+<g id="a_node80"><a xlink:title="Es_fv_both theory/NamedMeta.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-2615" rx="35.44" ry="18"/>
+<text text-anchor="middle" x="408.74" y="-2612.8" font-family="Inter" font-size="9.00" fill="#222222">Es_fv_both</text>
+</a>
+</g>
+</g>
+<!-- nplug_fv_mono&#45;&gt;Es_fv_both -->
+<g id="edge55" class="edge">
+<title>nplug_fv_mono&#45;&gt;Es_fv_both</title>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M272.26,-2671.02C301.65,-2658.87 345.37,-2640.79 375.14,-2628.48"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="376.16,-2630.33 380.9,-2626.1 374.55,-2626.45 376.16,-2630.33"/>
 </g>
 <!-- nplug_fv_upper&#45;&gt;nred_core_fv -->
 <g id="edge46" class="edge">
 <title>nplug_fv_upper&#45;&gt;nred_core_fv</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M282.12,-2719.58C307.32,-2715.05 339.48,-2709.27 364.95,-2704.69"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="365.41,-2706.74 370.94,-2703.62 364.67,-2702.61 365.41,-2706.74"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M272.26,-2757.02C300.85,-2745.2 343.01,-2727.77 372.69,-2715.49"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="373.71,-2717.34 378.45,-2713.11 372.1,-2713.46 373.71,-2717.34"/>
 </g>
 <!-- nplug_fv_upper&#45;&gt;nred_fv -->
 <g id="edge53" class="edge">
 <title>nplug_fv_upper&#45;&gt;nred_fv</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M278.74,-2736.76C308.42,-2744.41 349.2,-2754.91 376.9,-2762.05"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="376.62,-2764.15 382.95,-2763.61 377.67,-2760.08 376.62,-2764.15"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M286.47,-2770C314.58,-2770 349.96,-2770 375.24,-2770"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="375.44,-2772.1 381.44,-2770 375.44,-2767.9 375.44,-2772.1"/>
 </g>
 <!-- nplug_esub_fv&#45;&gt;nred_fv -->
 <g id="edge51" class="edge">
 <title>nplug_esub_fv&#45;&gt;nred_fv</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M277.5,-2803.56C307.28,-2795.89 348.85,-2785.18 376.94,-2777.94"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="377.79,-2779.89 383.08,-2776.36 376.74,-2775.82 377.79,-2779.89"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M275.45,-2811.23C305.75,-2801.78 349.33,-2788.2 378.07,-2779.25"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="378.87,-2781.2 383.97,-2777.41 377.62,-2777.19 378.87,-2781.2"/>
+</g>
+<!-- in_filter_neq_iff -->
+<g id="node79" class="node">
+<title>in_filter_neq_iff</title>
+<g id="a_node79"><a xlink:title="in_filter_neq_iff theory/NamedMeta.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-2598" rx="46.38" ry="18"/>
+<text text-anchor="middle" x="239.88" y="-2595.8" font-family="Inter" font-size="9.00" fill="#222222">in_filter_neq_iff</text>
+</a>
+</g>
+</g>
+<!-- in_filter_neq_iff&#45;&gt;Es_fv_both -->
+<g id="edge54" class="edge">
+<title>in_filter_neq_iff&#45;&gt;Es_fv_both</title>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M284.72,-2602.47C310.44,-2605.09 342.71,-2608.37 367.74,-2610.92"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="367.76,-2613.04 373.94,-2611.56 368.18,-2608.86 367.76,-2613.04"/>
+</g>
+<!-- Es_fv -->
+<g id="node81" class="node">
+<title>Es_fv</title>
+<g id="a_node81"><a xlink:title="Es_fv theory/NamedMeta.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="578.76" cy="-2615" rx="27" ry="18"/>
+<text text-anchor="middle" x="578.76" y="-2612.8" font-family="Inter" font-size="9.00" fill="#222222">Es_fv</text>
+</a>
+</g>
+</g>
+<!-- Es_fv_both&#45;&gt;Es_fv -->
+<g id="edge56" class="edge">
+<title>Es_fv_both&#45;&gt;Es_fv</title>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M444.14,-2615C473.78,-2615 516.24,-2615 545.29,-2615"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="545.64,-2617.1 551.64,-2615 545.64,-2612.9 545.64,-2617.1"/>
 </g>
 <!-- par_red1_iff -->
-<g id="node79" class="node">
+<g id="node82" class="node">
 <title>par_red1_iff</title>
-<g id="a_node79"><a xlink:title="par_red1_iff theory/Parallel.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-2959" rx="37.56" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-2956.8" font-family="Inter" font-size="9.00" fill="#222222">par_red1_iff</text>
+<g id="a_node82"><a xlink:title="par_red1_iff theory/Parallel.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-2968" rx="37.56" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-2965.8" font-family="Inter" font-size="9.00" fill="#222222">par_red1_iff</text>
 </a>
 </g>
 </g>
 <!-- par_to_red1_or_eq -->
-<g id="node82" class="node">
+<g id="node85" class="node">
 <title>par_to_red1_or_eq</title>
-<g id="a_node82"><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="-2985" rx="53.23" ry="18"/>
-<text text-anchor="middle" x="239.88" y="-2982.8" font-family="Inter" font-size="9.00" fill="#222222">par_to_red1_or_eq</text>
+<g id="a_node85"><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="-2994" rx="53.23" ry="18"/>
+<text text-anchor="middle" x="239.88" y="-2991.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="edge54" class="edge">
+<g id="edge57" 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,-2964.26C125.17,-2967.88 157.5,-2972.74 184.81,-2976.86"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="184.66,-2978.96 190.91,-2977.78 185.29,-2974.81 184.66,-2978.96"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M101.18,-2973.26C125.17,-2976.88 157.5,-2981.74 184.81,-2985.86"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="184.66,-2987.96 190.91,-2986.78 185.29,-2983.81 184.66,-2987.96"/>
 </g>
 <!-- red1_or_eq_to_par -->
-<g id="node83" class="node">
+<g id="node86" class="node">
 <title>red1_or_eq_to_par</title>
-<g id="a_node83"><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="-2933" rx="53.23" ry="18"/>
-<text text-anchor="middle" x="239.88" y="-2930.8" font-family="Inter" font-size="9.00" fill="#222222">red1_or_eq_to_par</text>
+<g id="a_node86"><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="-2942" rx="53.23" ry="18"/>
+<text text-anchor="middle" x="239.88" y="-2939.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="edge55" class="edge">
+<g id="edge58" 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,-2953.74C125.17,-2950.12 157.5,-2945.26 184.81,-2941.14"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="185.29,-2943.19 190.91,-2940.22 184.66,-2939.04 185.29,-2943.19"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M101.18,-2962.74C125.17,-2959.12 157.5,-2954.26 184.81,-2950.14"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="185.29,-2952.19 190.91,-2949.22 184.66,-2948.04 185.29,-2952.19"/>
 </g>
 <!-- red1_in_par -->
-<g id="node80" class="node">
+<g id="node83" class="node">
 <title>red1_in_par</title>
-<g id="a_node80"><a xlink:title="red1_in_par theory/Parallel.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-3011" rx="37.56" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-3008.8" font-family="Inter" font-size="9.00" fill="#222222">red1_in_par</text>
+<g id="a_node83"><a xlink:title="red1_in_par theory/Parallel.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-3020" rx="37.56" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-3017.8" font-family="Inter" font-size="9.00" fill="#222222">red1_in_par</text>
 </a>
 </g>
 </g>
 <!-- par_context -->
-<g id="node81" class="node">
+<g id="node84" class="node">
 <title>par_context</title>
-<g id="a_node81"><a xlink:title="par_context theory/Parallel.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-3063" rx="38.87" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-3060.8" font-family="Inter" font-size="9.00" fill="#222222">par_context</text>
+<g id="a_node84"><a xlink:title="par_context theory/Parallel.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-3072" rx="38.87" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-3069.8" font-family="Inter" font-size="9.00" fill="#222222">par_context</text>
 </a>
 </g>
 </g>
 <!-- par_reflexive -->
-<g id="node84" class="node">
+<g id="node87" class="node">
 <title>par_reflexive</title>
-<g id="a_node84"><a xlink:title="par_reflexive theory/Parallel.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-3115" rx="41.64" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-3112.8" font-family="Inter" font-size="9.00" fill="#222222">par_reflexive</text>
+<g id="a_node87"><a xlink:title="par_reflexive theory/Parallel.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-3124" rx="41.64" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-3121.8" font-family="Inter" font-size="9.00" fill="#222222">par_reflexive</text>
 </a>
 </g>
 </g>
 <!-- gen_list_length -->
-<g id="node85" class="node">
+<g id="node88" class="node">
 <title>gen_list_length</title>
-<g id="a_node85"><a xlink:title="gen_list_length theory/Random.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-3167" rx="46.38" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-3164.8" font-family="Inter" font-size="9.00" fill="#222222">gen_list_length</text>
+<g id="a_node88"><a xlink:title="gen_list_length theory/Random.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-3176" rx="46.38" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-3173.8" font-family="Inter" font-size="9.00" fill="#222222">gen_list_length</text>
 </a>
 </g>
 </g>
 <!-- check_term_true -->
-<g id="node86" class="node">
+<g id="node89" class="node">
 <title>check_term_true</title>
-<g id="a_node86"><a xlink:title="check_term_true theory/Random.v https://arxiv.org/html/2312.13270v1">
+<g id="a_node89"><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="node87" class="node">
+<g id="node90" class="node">
 <title>check_all_true</title>
-<g id="a_node87"><a xlink:title="check_all_true theory/Random.v https://arxiv.org/html/2312.13270v1">
+<g id="a_node90"><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="edge58" class="edge">
+<g id="edge61" class="edge">
 <title>check_term_true&#45;&gt;check_all_true</title>
 <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"/>
@@ -1254,27 +1299,27 @@
 <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="node88" class="node">
+<g id="node91" class="node">
 <title>gen_sound</title>
-<g id="a_node88"><a xlink:title="gen_sound theory/Random.v https://arxiv.org/html/2312.13270v1">
+<g id="a_node91"><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="node89" class="node">
+<g id="node92" class="node">
 <title>gen_complete</title>
-<g id="a_node89"><a xlink:title="gen_complete theory/Random.v https://arxiv.org/html/2312.13270v1">
+<g id="a_node92"><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="node91" class="node">
+<g id="node94" class="node">
 <title>zdecs_sound</title>
-<g id="a_node91"><a xlink:title="zdecs_sound theory/Reduction.v https://arxiv.org/html/2312.13270v1">
+<g id="a_node94"><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>
@@ -1287,91 +1332,91 @@
 <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="node94" class="node">
+<g id="node97" class="node">
 <title>root_steps_sound</title>
-<g id="a_node94"><a xlink:title="root_steps_sound theory/Reduction.v https://arxiv.org/html/2312.13270v1">
+<g id="a_node97"><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="edge63" class="edge">
+<g id="edge66" class="edge">
 <title>zdecs_sound&#45;&gt;root_steps_sound</title>
 <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="edge98" class="edge">
+<g id="edge101" class="edge">
 <title>zdecs_sound&#45;&gt;full_comp_aux_sub</title>
 <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="node92" class="node">
+<g id="node95" class="node">
 <title>zdecs_complete</title>
-<g id="a_node92"><a xlink:title="zdecs_complete theory/Reduction.v https://arxiv.org/html/2312.13270v1">
+<g id="a_node95"><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="node95" class="node">
+<g id="node98" class="node">
 <title>root_steps_complete</title>
-<g id="a_node95"><a xlink:title="root_steps_complete theory/Reduction.v https://arxiv.org/html/2312.13270v1">
+<g id="a_node98"><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="edge64" class="edge">
+<g id="edge67" class="edge">
 <title>zdecs_complete&#45;&gt;root_steps_complete</title>
 <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="node93" class="node">
+<g id="node96" class="node">
 <title>positions_at</title>
-<g id="a_node93"><a xlink:title="positions_at theory/Reduction.v https://arxiv.org/html/2312.13270v1">
+<g id="a_node96"><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="node96" class="node">
+<g id="node99" class="node">
 <title>steps_sound</title>
-<g id="a_node96"><a xlink:title="steps_sound theory/Reduction.v https://arxiv.org/html/2312.13270v1">
+<g id="a_node99"><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="edge65" class="edge">
+<g id="edge68" class="edge">
 <title>positions_at&#45;&gt;steps_sound</title>
 <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="edge66" class="edge">
+<g id="edge69" class="edge">
 <title>root_steps_sound&#45;&gt;steps_sound</title>
 <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="node103" class="node">
+<g id="node106" class="node">
 <title>steps_complete</title>
-<g id="a_node103"><a xlink:title="steps_complete theory/Reduction.v https://arxiv.org/html/2312.13270v1">
+<g id="a_node106"><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="edge72" class="edge">
+<g id="edge75" class="edge">
 <title>root_steps_complete&#45;&gt;steps_complete</title>
 <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"/>
@@ -1383,160 +1428,160 @@
 <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="edge59" class="edge">
+<g id="edge62" class="edge">
 <title>steps_sound&#45;&gt;gen_sound</title>
 <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="node97" class="node">
+<g id="node100" class="node">
 <title>steps_sound_red1</title>
-<g id="a_node97"><a xlink:title="steps_sound_red1 theory/Reduction.v https://arxiv.org/html/2312.13270v1">
+<g id="a_node100"><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="edge67" class="edge">
+<g id="edge70" class="edge">
 <title>steps_sound&#45;&gt;steps_sound_red1</title>
 <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="node105" class="node">
+<g id="node108" class="node">
 <title>has_red_spec</title>
-<g id="a_node105"><a xlink:title="has_red_spec theory/Reduction.v https://arxiv.org/html/2312.13270v1">
+<g id="a_node108"><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="edge76" class="edge">
+<g id="edge79" class="edge">
 <title>steps_sound&#45;&gt;has_red_spec</title>
 <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="node140" class="node">
+<g id="node143" class="node">
 <title>corpus_sound</title>
-<g id="a_node140"><a xlink:title="corpus_sound theory/Tests.v https://arxiv.org/html/2312.13270v1">
+<g id="a_node143"><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="edge105" class="edge">
+<g id="edge108" class="edge">
 <title>steps_sound&#45;&gt;corpus_sound</title>
 <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="edge57" class="edge">
+<g id="edge60" class="edge">
 <title>steps_sound_red1&#45;&gt;check_term_true</title>
 <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="edge62" class="edge">
+<g id="edge65" class="edge">
 <title>steps_sound_red1&#45;&gt;gen_fv_preserved</title>
 <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="node107" class="node">
+<g id="node110" class="node">
 <title>nf_iff_steps_nil</title>
-<g id="a_node107"><a xlink:title="nf_iff_steps_nil theory/Reduction.v https://arxiv.org/html/2312.13270v1">
+<g id="a_node110"><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="edge79" class="edge">
+<g id="edge82" class="edge">
 <title>steps_sound_red1&#45;&gt;nf_iff_steps_nil</title>
 <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="edge109" class="edge">
+<g id="edge112" class="edge">
 <title>steps_sound_red1&#45;&gt;corpus_fv_preserved</title>
 <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="node98" class="node">
+<g id="node101" class="node">
 <title>positions_hole</title>
-<g id="a_node98"><a xlink:title="positions_hole theory/Reduction.v https://arxiv.org/html/2312.13270v1">
+<g id="a_node101"><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="node99" class="node">
+<g id="node102" class="node">
 <title>root_steps_in_steps</title>
-<g id="a_node99"><a xlink:title="root_steps_in_steps theory/Reduction.v https://arxiv.org/html/2312.13270v1">
+<g id="a_node102"><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="edge68" class="edge">
+<g id="edge71" class="edge">
 <title>positions_hole&#45;&gt;root_steps_in_steps</title>
 <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="edge73" class="edge">
+<g id="edge76" class="edge">
 <title>root_steps_in_steps&#45;&gt;steps_complete</title>
 <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="node100" class="node">
+<g id="node103" class="node">
 <title>plug_comp</title>
-<g id="a_node100"><a xlink:title="plug_comp theory/Reduction.v https://arxiv.org/html/2312.13270v1">
+<g id="a_node103"><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="edge70" class="edge">
+<g id="edge73" class="edge">
 <title>plug_comp&#45;&gt;steps_complete</title>
 <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="node101" class="node">
+<g id="node104" class="node">
 <title>positions_comp</title>
-<g id="a_node101"><a xlink:title="positions_comp theory/Reduction.v https://arxiv.org/html/2312.13270v1">
+<g id="a_node104"><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="edge71" class="edge">
+<g id="edge74" class="edge">
 <title>positions_comp&#45;&gt;steps_complete</title>
 <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="node102" class="node">
+<g id="node105" class="node">
 <title>at_ctx_comp</title>
-<g id="a_node102"><a xlink:title="at_ctx_comp theory/Reduction.v https://arxiv.org/html/2312.13270v1">
+<g id="a_node105"><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="edge69" class="edge">
+<g id="edge72" class="edge">
 <title>at_ctx_comp&#45;&gt;steps_complete</title>
 <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"/>
@@ -1548,415 +1593,415 @@
 <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="edge60" class="edge">
+<g id="edge63" class="edge">
 <title>steps_complete&#45;&gt;gen_complete</title>
 <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="edge75" class="edge">
+<g id="edge78" class="edge">
 <title>steps_complete&#45;&gt;has_red_spec</title>
 <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="edge78" class="edge">
+<g id="edge81" class="edge">
 <title>steps_complete&#45;&gt;nf_iff_steps_nil</title>
 <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="node141" class="node">
+<g id="node144" class="node">
 <title>corpus_complete</title>
-<g id="a_node141"><a xlink:title="corpus_complete theory/Tests.v https://arxiv.org/html/2312.13270v1">
+<g id="a_node144"><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="edge106" class="edge">
+<g id="edge109" class="edge">
 <title>steps_complete&#45;&gt;corpus_complete</title>
 <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="node104" class="node">
+<g id="node107" class="node">
 <title>has_red_f</title>
-<g id="a_node104"><a xlink:title="has_red_f theory/Reduction.v https://arxiv.org/html/2312.13270v1">
+<g id="a_node107"><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="edge74" class="edge">
+<g id="edge77" class="edge">
 <title>has_red_f&#45;&gt;has_red_spec</title>
 <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="edge56" class="edge">
+<g id="edge59" class="edge">
 <title>has_red_spec&#45;&gt;check_term_true</title>
 <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="node106" class="node">
+<g id="node109" class="node">
 <title>red1_dec</title>
-<g id="a_node106"><a xlink:title="red1_dec theory/Reduction.v https://arxiv.org/html/2312.13270v1">
+<g id="a_node109"><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="edge77" class="edge">
+<g id="edge80" class="edge">
 <title>has_red_spec&#45;&gt;red1_dec</title>
 <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="node142" class="node">
+<g id="node145" class="node">
 <title>corpus_decides</title>
-<g id="a_node142"><a xlink:title="corpus_decides theory/Tests.v https://arxiv.org/html/2312.13270v1">
+<g id="a_node145"><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="edge107" class="edge">
+<g id="edge110" class="edge">
 <title>has_red_spec&#45;&gt;corpus_decides</title>
 <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="node108" class="node">
+<g id="node111" class="node">
 <title>normal_form_iff_nf</title>
-<g id="a_node108"><a xlink:title="normal_form_iff_nf theory/Reduction.v https://arxiv.org/html/2312.13270v1">
+<g id="a_node111"><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="edge80" class="edge">
+<g id="edge83" class="edge">
 <title>nf_iff_steps_nil&#45;&gt;normal_form_iff_nf</title>
 <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="node109" class="node">
+<g id="node112" class="node">
 <title>nf_dec</title>
-<g id="a_node109"><a xlink:title="nf_dec theory/Reduction.v https://arxiv.org/html/2312.13270v1">
+<g id="a_node112"><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="edge81" class="edge">
+<g id="edge84" class="edge">
 <title>nf_iff_steps_nil&#45;&gt;nf_dec</title>
 <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="node110" class="node">
+<g id="node113" class="node">
 <title>open_rec_app</title>
-<g id="a_node110"><a xlink:title="open_rec_app theory/Substitution.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-3219" rx="43.1" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-3216.8" font-family="Inter" font-size="9.00" fill="#222222">open_rec_app</text>
+<g id="a_node113"><a xlink:title="open_rec_app theory/Substitution.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-3228" rx="43.1" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-3225.8" font-family="Inter" font-size="9.00" fill="#222222">open_rec_app</text>
 </a>
 </g>
 </g>
 <!-- open_rec_lam -->
-<g id="node111" class="node">
+<g id="node114" class="node">
 <title>open_rec_lam</title>
-<g id="a_node111"><a xlink:title="open_rec_lam theory/Substitution.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-3271" rx="43.76" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-3268.8" font-family="Inter" font-size="9.00" fill="#222222">open_rec_lam</text>
+<g id="a_node114"><a xlink:title="open_rec_lam theory/Substitution.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-3280" rx="43.76" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-3277.8" font-family="Inter" font-size="9.00" fill="#222222">open_rec_lam</text>
 </a>
 </g>
 </g>
 <!-- open_rec_esub -->
-<g id="node112" class="node">
+<g id="node115" class="node">
 <title>open_rec_esub</title>
-<g id="a_node112"><a xlink:title="open_rec_esub theory/Substitution.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-3323" rx="46.38" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-3320.8" font-family="Inter" font-size="9.00" fill="#222222">open_rec_esub</text>
+<g id="a_node115"><a xlink:title="open_rec_esub theory/Substitution.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-3332" rx="46.38" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-3329.8" font-family="Inter" font-size="9.00" fill="#222222">open_rec_esub</text>
 </a>
 </g>
 </g>
 <!-- close_rec_app -->
-<g id="node113" class="node">
+<g id="node116" class="node">
 <title>close_rec_app</title>
-<g id="a_node113"><a xlink:title="close_rec_app theory/Substitution.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-3375" rx="44.41" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-3372.8" font-family="Inter" font-size="9.00" fill="#222222">close_rec_app</text>
+<g id="a_node116"><a xlink:title="close_rec_app theory/Substitution.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-3384" rx="44.41" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-3381.8" font-family="Inter" font-size="9.00" fill="#222222">close_rec_app</text>
 </a>
 </g>
 </g>
 <!-- close_rec_lam -->
-<g id="node114" class="node">
+<g id="node117" class="node">
 <title>close_rec_lam</title>
-<g id="a_node114"><a xlink:title="close_rec_lam theory/Substitution.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-3427" rx="44.41" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-3424.8" font-family="Inter" font-size="9.00" fill="#222222">close_rec_lam</text>
+<g id="a_node117"><a xlink:title="close_rec_lam theory/Substitution.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-3436" rx="44.41" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-3433.8" font-family="Inter" font-size="9.00" fill="#222222">close_rec_lam</text>
 </a>
 </g>
 </g>
 <!-- close_rec_esub -->
-<g id="node115" class="node">
+<g id="node118" class="node">
 <title>close_rec_esub</title>
-<g id="a_node115"><a xlink:title="close_rec_esub theory/Substitution.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-3479" rx="46.53" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-3476.8" font-family="Inter" font-size="9.00" fill="#222222">close_rec_esub</text>
+<g id="a_node118"><a xlink:title="close_rec_esub theory/Substitution.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-3488" rx="46.53" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-3485.8" font-family="Inter" font-size="9.00" fill="#222222">close_rec_esub</text>
 </a>
 </g>
 </g>
 <!-- subst_app -->
-<g id="node116" class="node">
+<g id="node119" class="node">
 <title>subst_app</title>
-<g id="a_node116"><a xlink:title="subst_app theory/Substitution.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-3531" rx="34.13" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-3528.8" font-family="Inter" font-size="9.00" fill="#222222">subst_app</text>
+<g id="a_node119"><a xlink:title="subst_app theory/Substitution.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-3540" rx="34.13" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-3537.8" font-family="Inter" font-size="9.00" fill="#222222">subst_app</text>
 </a>
 </g>
 </g>
 <!-- subst_lam -->
-<g id="node117" class="node">
+<g id="node120" class="node">
 <title>subst_lam</title>
-<g id="a_node117"><a xlink:title="subst_lam theory/Substitution.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-3583" rx="34.13" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-3580.8" font-family="Inter" font-size="9.00" fill="#222222">subst_lam</text>
+<g id="a_node120"><a xlink:title="subst_lam theory/Substitution.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-3592" rx="34.13" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-3589.8" font-family="Inter" font-size="9.00" fill="#222222">subst_lam</text>
 </a>
 </g>
 </g>
 <!-- subst_esub -->
-<g id="node118" class="node">
+<g id="node121" class="node">
 <title>subst_esub</title>
-<g id="a_node118"><a xlink:title="subst_esub theory/Substitution.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-3635" rx="36.25" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-3632.8" font-family="Inter" font-size="9.00" fill="#222222">subst_esub</text>
+<g id="a_node121"><a xlink:title="subst_esub theory/Substitution.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-3644" rx="36.25" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-3641.8" font-family="Inter" font-size="9.00" fill="#222222">subst_esub</text>
 </a>
 </g>
 </g>
 <!-- open_rec_lc_atom -->
-<g id="node122" class="node">
+<g id="node125" class="node">
 <title>open_rec_lc_atom</title>
-<g id="a_node122"><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="-3687" rx="53.89" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-3684.8" font-family="Inter" font-size="9.00" fill="#222222">open_rec_lc_atom</text>
+<g id="a_node125"><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="-3696" rx="53.89" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-3693.8" font-family="Inter" font-size="9.00" fill="#222222">open_rec_lc_atom</text>
 </a>
 </g>
 </g>
 <!-- open_rec_lc -->
-<g id="node123" class="node">
+<g id="node126" class="node">
 <title>open_rec_lc</title>
-<g id="a_node123"><a xlink:title="open_rec_lc theory/Substitution.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-3687" rx="39.02" ry="18"/>
-<text text-anchor="middle" x="239.88" y="-3684.8" font-family="Inter" font-size="9.00" fill="#222222">open_rec_lc</text>
+<g id="a_node126"><a xlink:title="open_rec_lc theory/Substitution.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-3696" rx="39.02" ry="18"/>
+<text text-anchor="middle" x="239.88" y="-3693.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="edge86" class="edge">
+<g id="edge89" 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,-3687C143.1,-3687 171.36,-3687 194.39,-3687"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="194.43,-3689.1 200.43,-3687 194.43,-3684.9 194.43,-3689.1"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M118.98,-3696C143.1,-3696 171.36,-3696 194.39,-3696"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="194.43,-3698.1 200.43,-3696 194.43,-3693.9 194.43,-3698.1"/>
 </g>
 <!-- red_sub_root_to_red1 -->
-<g id="node124" class="node">
+<g id="node127" class="node">
 <title>red_sub_root_to_red1</title>
-<g id="a_node124"><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="-3739" rx="60.09" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-3736.8" font-family="Inter" font-size="9.00" fill="#222222">red_sub_root_to_red1</text>
+<g id="a_node127"><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="-3748" rx="60.09" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-3745.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="node125" class="node">
+<g id="node128" class="node">
 <title>red_sub_to_red1</title>
-<g id="a_node125"><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="-3739" rx="47.84" ry="18"/>
-<text text-anchor="middle" x="239.88" y="-3736.8" font-family="Inter" font-size="9.00" fill="#222222">red_sub_to_red1</text>
+<g id="a_node128"><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="-3748" rx="47.84" ry="18"/>
+<text text-anchor="middle" x="239.88" y="-3745.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="edge87" class="edge">
+<g id="edge90" 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,-3739C145.11,-3739 166.58,-3739 185.56,-3739"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="185.89,-3741.1 191.89,-3739 185.89,-3736.9 185.89,-3741.1"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M125.65,-3748C145.11,-3748 166.58,-3748 185.56,-3748"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="185.89,-3750.1 191.89,-3748 185.89,-3745.9 185.89,-3750.1"/>
 </g>
 <!-- red_sub_context -->
-<g id="node126" class="node">
+<g id="node129" class="node">
 <title>red_sub_context</title>
-<g id="a_node126"><a xlink:title="red_sub_context theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-3791" rx="49.15" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-3788.8" font-family="Inter" font-size="9.00" fill="#222222">red_sub_context</text>
+<g id="a_node129"><a xlink:title="red_sub_context theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-3800" rx="49.15" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-3797.8" font-family="Inter" font-size="9.00" fill="#222222">red_sub_context</text>
 </a>
 </g>
 </g>
 <!-- Star_red_sub_context -->
-<g id="node132" class="node">
+<g id="node135" class="node">
 <title>Star_red_sub_context</title>
-<g id="a_node132"><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="-3791" rx="61.55" ry="18"/>
-<text text-anchor="middle" x="239.88" y="-3788.8" font-family="Inter" font-size="9.00" fill="#222222">Star_red_sub_context</text>
+<g id="a_node135"><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="-3800" rx="61.55" ry="18"/>
+<text text-anchor="middle" x="239.88" y="-3797.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="edge90" class="edge">
+<g id="edge93" 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,-3791C132.08,-3791 152.53,-3791 171.66,-3791"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="172.09,-3793.1 178.09,-3791 172.09,-3788.9 172.09,-3793.1"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M114.33,-3800C132.08,-3800 152.53,-3800 171.66,-3800"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="172.09,-3802.1 178.09,-3800 172.09,-3797.9 172.09,-3802.1"/>
 </g>
 <!-- red_sub_gc -->
-<g id="node127" class="node">
+<g id="node130" class="node">
 <title>red_sub_gc</title>
-<g id="a_node127"><a xlink:title="red_sub_gc theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
+<g id="a_node130"><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="edge95" class="edge">
+<g id="edge98" class="edge">
 <title>red_sub_gc&#45;&gt;full_comp_aux_sub</title>
 <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="node139" class="node">
+<g id="node142" class="node">
 <title>red_gc_to_red_sub</title>
-<g id="a_node139"><a xlink:title="red_gc_to_red_sub theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
+<g id="a_node142"><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="edge104" class="edge">
+<g id="edge107" 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="node128" class="node">
+<g id="node131" class="node">
 <title>red_sub_r</title>
-<g id="a_node128"><a xlink:title="red_sub_r theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
+<g id="a_node131"><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="edge96" class="edge">
+<g id="edge99" class="edge">
 <title>red_sub_r&#45;&gt;full_comp_aux_sub</title>
 <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="node129" class="node">
+<g id="node132" class="node">
 <title>occurs_zfill</title>
-<g id="a_node129"><a xlink:title="occurs_zfill theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-3843" rx="37.56" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-3840.8" font-family="Inter" font-size="9.00" fill="#222222">occurs_zfill</text>
+<g id="a_node132"><a xlink:title="occurs_zfill theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="65.24" cy="-3852" rx="37.56" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-3849.8" font-family="Inter" font-size="9.00" fill="#222222">occurs_zfill</text>
 </a>
 </g>
 </g>
 <!-- zfill_occurs0 -->
-<g id="node130" class="node">
+<g id="node133" class="node">
 <title>zfill_occurs0</title>
-<g id="a_node130"><a xlink:title="zfill_occurs0 theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-3843" rx="40.98" ry="18"/>
-<text text-anchor="middle" x="239.88" y="-3840.8" font-family="Inter" font-size="9.00" fill="#222222">zfill_occurs0</text>
+<g id="a_node133"><a xlink:title="zfill_occurs0 theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-3852" rx="40.98" ry="18"/>
+<text text-anchor="middle" x="239.88" y="-3849.8" font-family="Inter" font-size="9.00" fill="#222222">zfill_occurs0</text>
 </a>
 </g>
 </g>
 <!-- occurs_zfill&#45;&gt;zfill_occurs0 -->
-<g id="edge88" class="edge">
+<g id="edge91" class="edge">
 <title>occurs_zfill&#45;&gt;zfill_occurs0</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M102.85,-3843C128.98,-3843 164.34,-3843 192.45,-3843"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="192.7,-3845.1 198.7,-3843 192.7,-3840.9 192.7,-3845.1"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M102.85,-3852C128.98,-3852 164.34,-3852 192.45,-3852"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="192.7,-3854.1 198.7,-3852 192.7,-3849.9 192.7,-3854.1"/>
 </g>
 <!-- R_Gc_disjoint -->
-<g id="node131" class="node">
+<g id="node134" class="node">
 <title>R_Gc_disjoint</title>
-<g id="a_node131"><a xlink:title="R_Gc_disjoint theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-3843" rx="41.64" ry="18"/>
-<text text-anchor="middle" x="408.74" y="-3840.8" font-family="Inter" font-size="9.00" fill="#222222">R_Gc_disjoint</text>
+<g id="a_node134"><a xlink:title="R_Gc_disjoint theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-3852" rx="41.64" ry="18"/>
+<text text-anchor="middle" x="408.74" y="-3849.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="edge89" class="edge">
+<g id="edge92" class="edge">
 <title>zfill_occurs0&#45;&gt;R_Gc_disjoint</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M281.27,-3843C305.28,-3843 335.83,-3843 360.89,-3843"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="361.14,-3845.1 367.14,-3843 361.14,-3840.9 361.14,-3845.1"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M281.27,-3852C305.28,-3852 335.83,-3852 360.89,-3852"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="361.14,-3854.1 367.14,-3852 361.14,-3849.9 361.14,-3854.1"/>
 </g>
 <!-- plus_red_sub_full_comp -->
-<g id="node134" class="node">
+<g id="node137" class="node">
 <title>plus_red_sub_full_comp</title>
-<g id="a_node134"><a xlink:title="plus_red_sub_full_comp theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
+<g id="a_node137"><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="edge99" class="edge">
+<g id="edge102" 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="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="edge101" class="edge">
+<g id="edge104" 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="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="node136" class="node">
+<g id="node139" class="node">
 <title>es_count_plug_mono</title>
-<g id="a_node136"><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="-3895" rx="60.74" ry="18"/>
-<text text-anchor="middle" x="65.24" y="-3892.8" font-family="Inter" font-size="9.00" fill="#222222">es_count_plug_mono</text>
+<g id="a_node139"><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="-3904" rx="60.74" ry="18"/>
+<text text-anchor="middle" x="65.24" y="-3901.8" font-family="Inter" font-size="9.00" fill="#222222">es_count_plug_mono</text>
 </a>
 </g>
 </g>
 <!-- red_gc_measure -->
-<g id="node137" class="node">
+<g id="node140" class="node">
 <title>red_gc_measure</title>
-<g id="a_node137"><a xlink:title="red_gc_measure theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-3895" rx="49.8" ry="18"/>
-<text text-anchor="middle" x="239.88" y="-3892.8" font-family="Inter" font-size="9.00" fill="#222222">red_gc_measure</text>
+<g id="a_node140"><a xlink:title="red_gc_measure theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="239.88" cy="-3904" rx="49.8" ry="18"/>
+<text text-anchor="middle" x="239.88" y="-3901.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="edge102" class="edge">
+<g id="edge105" 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,-3895C144.95,-3895 165.61,-3895 184.05,-3895"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="184.22,-3897.1 190.22,-3895 184.22,-3892.9 184.22,-3897.1"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M126.14,-3904C144.95,-3904 165.61,-3904 184.05,-3904"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="184.22,-3906.1 190.22,-3904 184.22,-3901.9 184.22,-3906.1"/>
 </g>
 <!-- red_gc_terminates -->
-<g id="node138" class="node">
+<g id="node141" class="node">
 <title>red_gc_terminates</title>
-<g id="a_node138"><a xlink:title="red_gc_terminates theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
-<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-3895" rx="54.04" ry="18"/>
-<text text-anchor="middle" x="408.74" y="-3892.8" font-family="Inter" font-size="9.00" fill="#222222">red_gc_terminates</text>
+<g id="a_node141"><a xlink:title="red_gc_terminates theory/Subsystem.v https://arxiv.org/html/2312.13270v1">
+<ellipse fill="#d9ead3" stroke="#38761d" cx="408.74" cy="-3904" rx="54.04" ry="18"/>
+<text text-anchor="middle" x="408.74" y="-3901.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="edge103" class="edge">
+<g id="edge106" class="edge">
 <title>red_gc_measure&#45;&gt;red_gc_terminates</title>
-<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M289.59,-3895C307.82,-3895 328.75,-3895 347.88,-3895"/>
-<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="348.29,-3897.1 354.29,-3895 348.29,-3892.9 348.29,-3897.1"/>
+<path fill="none" stroke="#9a9a9a" stroke-width="0.8" d="M289.59,-3904C307.82,-3904 328.75,-3904 347.88,-3904"/>
+<polygon fill="#9a9a9a" stroke="#9a9a9a" stroke-width="0.8" points="348.29,-3906.1 354.29,-3904 348.29,-3901.9 348.29,-3906.1"/>
 </g>
 </g>
 </svg>
diff --git a/graphs/index.txt b/graphs/index.txt
index fc0b942..331c76b 100644
--- a/graphs/index.txt
+++ b/graphs/index.txt
@@ -1,5 +1,7 @@
 status	milestone	kind	name	file
 proved	M0	infra	Es_ctx_any	theory/NamedMeta.v
+proved	M0	infra	Es_fv	theory/NamedMeta.v
+proved	M0	infra	Es_fv_both	theory/NamedMeta.v
 proved	M0	infra	Es_refl_any	theory/NamedMeta.v
 proved	M0	infra	Es_sym_any	theory/NamedMeta.v
 proved	M0	infra	Es_trans_any	theory/NamedMeta.v
@@ -7,6 +9,7 @@ proved	M0	infra	Plus_mred_of_Plus_red1	theory/Metaterm.v
 proved	M0	infra	eqC_in_Es	theory/NamedMeta.v
 proved	M0	infra	filter_neq_in	theory/NamedMeta.v
 proved	M0	infra	in_filter_neq	theory/NamedMeta.v
+proved	M0	infra	in_filter_neq_iff	theory/NamedMeta.v
 proved	M0	infra	isubst_meta_in	theory/NamedMeta.v
 proved	M0	infra	isubst_meta_notin	theory/NamedMeta.v
 proved	M0	infra	mfvs_close_m	theory/Metaterm.v
diff --git a/graphs/theorems.json b/graphs/theorems.json
index 955bfce..7f6769c 100644
--- a/graphs/theorems.json
+++ b/graphs/theorems.json
@@ -879,6 +879,41 @@
         "nplug_fv_upper"
       ]
     },
+    {
+      "id": "in_filter_neq_iff",
+      "label": "in_filter_neq_iff",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M0",
+      "section": "",
+      "file": "theory/NamedMeta.v",
+      "depends": []
+    },
+    {
+      "id": "Es_fv_both",
+      "label": "Es_fv_both",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M0",
+      "section": "",
+      "file": "theory/NamedMeta.v",
+      "depends": [
+        "in_filter_neq_iff",
+        "nplug_fv_mono"
+      ]
+    },
+    {
+      "id": "Es_fv",
+      "label": "Es_fv",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M0",
+      "section": "",
+      "file": "theory/NamedMeta.v",
+      "depends": [
+        "Es_fv_both"
+      ]
+    },
     {
       "id": "par_red1_iff",
       "label": "par_red1_iff",
diff --git a/theory/NamedMeta.v b/theory/NamedMeta.v
index 7461724..acd0343 100644
--- a/theory/NamedMeta.v
+++ b/theory/NamedMeta.v
@@ -300,3 +300,58 @@ Qed.
 
 Print Assumptions nplug_esub_fv.
 Print Assumptions nred_fv.
+
+Lemma in_filter_neq_iff : forall z a l,
+  In z (filter (fun w => negb (Nat.eqb w a)) l) <-> In z l /\ z <> a.
+Proof.
+  intros z a l. split.
+  - intro H. apply filter_In in H. destruct H as [Hl Hp]. split; [exact Hl |].
+    apply Nat.eqb_neq. destruct (Nat.eqb z a) eqn:E; [| reflexivity].
+    simpl in Hp. discriminate Hp.
+  - intros [Hl Hne]. apply filter_In. split; [exact Hl |].
+    apply Nat.eqb_neq in Hne. rewrite Hne. reflexivity.
+Qed.
+
+Lemma Es_fv_both : forall t u, Es t u ->
+  incl (nfv t) (nfv u) /\ incl (nfv u) (nfv t).
+Proof.
+  apply Es_ind.
+  - intros t0. split; unfold incl; auto.
+  - intros t0 u0 H1 IH1. split.
+    + apply (proj2 IH1).
+    + apply (proj1 IH1).
+  - intros t0 u0 v0 H1 H2 IH1 IH2. split.
+    + intros z Hz. apply (proj1 IH2). apply (proj1 H2). exact Hz.
+    + intros z Hz. apply (proj2 H2). apply (proj2 IH2). exact Hz.
+  - intros t0 x0 u0 y0 v0 Hyx Hyu Hxv. split; unfold incl; intros z Hz; simpl in *;
+    apply in_app_iff in Hz as [Hz|Hz].
+    + apply in_filter_neq_iff in Hz as [Hz Hy]. apply in_app_iff in Hz as [Hz|Hz].
+      * apply in_filter_neq_iff in Hz as [Hz Hx].
+        apply in_app_iff. left. apply in_filter_neq_iff. split; [| exact Hx].
+        apply in_app_iff. left. apply in_filter_neq_iff. split; [exact Hz | exact Hy].
+      * apply in_app_iff. right. exact Hz.
+    + apply in_app_iff. left. apply in_filter_neq_iff. split; [| ].
+      * apply in_app_iff. right. exact Hz.
+      * intro E. apply Hxv. subst z. exact Hz.
+    + apply in_filter_neq_iff in Hz as [Hz Hx]. apply in_app_iff in Hz as [Hz|Hz].
+      * apply in_filter_neq_iff in Hz as [Hz Hy].
+        apply in_app_iff. left. apply in_filter_neq_iff. split; [| exact Hy].
+        apply in_app_iff. left. apply in_filter_neq_iff. split; [exact Hz | exact Hx].
+      * apply in_app_iff. right. exact Hz.
+    + apply in_app_iff. left. apply in_filter_neq_iff. split; [| ].
+      * apply in_app_iff. right. exact Hz.
+      * intro E. apply Hyu. subst z. exact Hz.
+  - intros C0 t0 t0' H1 IH1. split; apply nplug_fv_mono.
+    + apply (proj1 IH1).
+    + apply (proj2 IH1).
+Qed.
+
+Lemma Es_fv : forall t u, Es t u -> forall z, In z (nfv t) <-> In z (nfv u).
+Proof.
+  intros t u H z. destruct (Es_fv_both t u H) as [Htu Hut]. split.
+  - apply Htu.
+  - apply Hut.
+Qed.
+
+Print Assumptions in_filter_neq_iff.
+Print Assumptions Es_fv.