Add wff_SmartPairf_SmartValf

1 files changed, 9 insertions, 0 deletions

diff --git a/src/Compilers/WfProofs.v b/src/Compilers/WfProofs.v
index 463f86656..1d1cf87ad 100644
--- a/src/Compilers/WfProofs.v
+++ b/src/Compilers/WfProofs.v
@@ -168,6 +168,15 @@ Section language.
       induction t; try solve [ cbv [SmartPairf]; simpl; auto ].
       rewrite !SmartVarfMap_Pair, !SmartPairf_Pair; auto.
     Qed.
+
+    Lemma wff_SmartPairf_SmartValf G {t} f g
+          (Hfg : forall t, wff G (f t) (g t))
+      : wff G (t:=t) (var1:=var1) (var2:=var2)
+            (SmartPairf (SmartValf (fun t => exprf (Tbase t)) f _))
+            (SmartPairf (SmartValf (fun t => exprf (Tbase t)) g _)).
+    Proof.
+      induction t; try solve [ cbv [SmartPairf]; simpl; auto ].
+    Qed.
   End with_var.
 
   Definition duplicate_type {var1 var2}