Add eq_subst_types_pattern_collect_vars_empty_iff

1 files changed, 20 insertions, 0 deletions

diff --git a/src/Experiments/NewPipeline/RewriterWf1.v b/src/Experiments/NewPipeline/RewriterWf1.v
index 9342bfbd3..0536757e8 100644
--- a/src/Experiments/NewPipeline/RewriterWf1.v
+++ b/src/Experiments/NewPipeline/RewriterWf1.v
@@ -279,6 +279,16 @@ Module Compilers.
           congruence.
         Qed.
 
+        Lemma eq_subst_types_pattern_collect_vars_empty_iff pt evm (evm0:=PositiveMap.empty _)
+              (evm' := mk_new_evm evm (pattern.base.collect_vars pt) evm0)
+          : pattern.base.subst pt evm = pattern.base.subst pt evm'.
+        Proof using Type.
+          apply subst_eq_if_mem; subst evm' evm0; intro.
+          rewrite fold_right_evar_map_find_In, PositiveMap.gempty.
+          intro H; rewrite H.
+          break_innermost_match; reflexivity.
+        Qed.
+
         Lemma add_var_types_cps_id {t v evm T k}
         : @pattern.base.add_var_types_cps t v evm T k = k (@pattern.base.add_var_types_cps t v evm _ id).
         Proof using Type.
@@ -507,6 +517,16 @@ Module Compilers.
           congruence.
         Qed.
 
+        Lemma eq_subst_types_pattern_collect_vars_empty_iff pt evm (evm0:=PositiveMap.empty _)
+              (evm' := mk_new_evm evm (pattern.type.collect_vars pt) evm0)
+          : pattern.type.subst pt evm = pattern.type.subst pt evm'.
+        Proof using Type.
+          apply subst_eq_if_mem; subst evm' evm0; intro.
+          rewrite base.fold_right_evar_map_find_In, PositiveMap.gempty.
+          intro H; rewrite H.
+          break_innermost_match; reflexivity.
+        Qed.
+
         Lemma app_forall_vars_under_forall_vars_relation
               {p k1 k2 F v1 v2 evm}
           : @pattern.type.under_forall_vars_relation p k1 k2 F v1 v2