diff options
author | Jason Gross <jgross@mit.edu> | 2017-10-24 00:57:28 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-10-24 00:57:28 -0400 |
commit | f4d586d0747a0ae8cff02caf079453d3256b6436 (patch) | |
tree | c46430c79c03472e2fb01ed411446ee89930fd26 /src | |
parent | eb7cb9dbe4931d5ea142ba76630290abf1711520 (diff) |
Add wff_SmartPairf_SmartValf
Diffstat (limited to 'src')
-rw-r--r-- | src/Compilers/WfProofs.v | 9 |
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} |