Add wff_SmartPairf_SmartVarfMap_same

1 files changed, 10 insertions, 0 deletions

diff --git a/src/Compilers/WfProofs.v b/src/Compilers/WfProofs.v
index 5bf984a48..463f86656 100644
--- a/src/Compilers/WfProofs.v
+++ b/src/Compilers/WfProofs.v
@@ -158,6 +158,16 @@ Section language.
         induction Hwf; simpl in *; break_innermost_match; try congruence; eauto.
       Qed.
     End with_interp.
+
+    Lemma wff_SmartPairf_SmartVarfMap_same {var} G {t} v f g
+          (Hfg : forall t v, wff G (f t v) (g t v))
+      : wff G (t:=t) (var1:=var1) (var2:=var2)
+            (SmartPairf (SmartVarfMap f v))
+            (SmartPairf (SmartVarfMap (var:=var) g v)).
+    Proof.
+      induction t; try solve [ cbv [SmartPairf]; simpl; auto ].
+      rewrite !SmartVarfMap_Pair, !SmartPairf_Pair; auto.
+    Qed.
   End with_var.
 
   Definition duplicate_type {var1 var2}