Add UnderLets.wf_of_expr

1 files changed, 7 insertions, 0 deletions

diff --git a/src/UnderLetsProofs.v b/src/UnderLetsProofs.v
index 7a59b7c78..7553b2cb1 100644
--- a/src/UnderLetsProofs.v
+++ b/src/UnderLetsProofs.v
@@ -228,6 +228,13 @@ Module Compilers.
           intro Hwf; induction Hwf; cbn [to_expr]; [ assumption | constructor; auto ].
         Qed.
 
+        Lemma wf_of_expr {t} (x : @expr var1 t) (y : @expr var2 t)
+              G
+          : expr.wf G x y -> wf (fun G => expr.wf G) G (of_expr x) (of_expr y).
+        Proof.
+          intro Hwf; induction Hwf; cbn [of_expr]; repeat constructor; auto.
+        Qed.
+
         Lemma wf_splice {A1 B1 A2 B2}
               {P : list { t : type & var1 t * var2 t }%type -> A1 -> A2 -> Prop}
               {Q : list { t : type & var1 t * var2 t }%type -> B1 -> B2 -> Prop}