1 files changed, 30 insertions, 11 deletions
diff --git a/src/Compilers/Named/Wf.v b/src/Compilers/Named/Wf.v
index fec1de5ed..736d0bd81 100644
--- a/src/Compilers/Named/Wf.v
+++ b/src/Compilers/Named/Wf.v
@@ -1,3 +1,4 @@
+Require Import Crypto.Compilers.SmartMap.
 Require Import Crypto.Compilers.Syntax.
 Require Import Crypto.Compilers.Named.Context.
 Require Import Crypto.Compilers.Named.Syntax.
@@ -11,27 +12,45 @@ Module Export Named.
       Context {var}
               (Context : @Context base_type_code Name var).
 
-      Fixpoint wff (ctx : Context) {t} (e : @exprf base_type_code op Name t) : option pointed_Prop
-        := match e with
-           | TT => Some trivial
-           | Var t n => match lookupb ctx n t return bool with
-                        | Some _ => true
-                        | None => false
-                        end
-           | Op _ _ op args => @wff ctx _ args
-           | LetIn _ n ex _ eC => @wff ctx _ ex /\ inject (forall v, prop_of_option (@wff (extend ctx n v) _ eC))
-           | Pair _ ex _ ey => @wff ctx _ ex /\ @wff ctx _ ey
-           end%option_pointed_prop.
+      Section gen.
+        Context (quantify : forall tx, (interp_flat_type var tx -> option pointed_Prop) -> option pointed_Prop).
 
+        Fixpoint wff_gen (ctx : Context) {t} (e : @exprf base_type_code op Name t) : option pointed_Prop
+          := match e with
+             | TT => Some trivial
+             | Var t n => match lookupb ctx n t return bool with
+                          | Some _ => true
+                          | None => false
+                          end
+             | Op _ _ op args => @wff_gen ctx _ args
+             | LetIn _ n ex _ eC => @wff_gen ctx _ ex
+                                    /\ quantify _ (fun v => @wff_gen (extend ctx n v) _ eC)
+             | Pair _ ex _ ey => @wff_gen ctx _ ex /\ @wff_gen ctx _ ey
+             end%option_pointed_prop.
+      End gen.
+
+      Definition wff := wff_gen (fun tx f => inject (forall v, prop_of_option (f v))).
       Definition wf (ctx : Context) {t} (e : @expr base_type_code op Name t) : Prop
         := forall v, prop_of_option (@wff (extend ctx (Abs_name e) v) _ (invert_Abs e)).
     End with_var.
 
+    Section unit.
+      Context (Context : @Context base_type_code Name (fun _ => unit)).
+
+      Local Notation TT := (SmartValf _ (fun _ => tt) _).
+      Definition wff_unit := wff_gen Context (fun tx f => f TT).
+      Definition wf_unit ctx {t} (e : @expr base_type_code op Name t) : option pointed_Prop
+        := @wff_unit (extend ctx (Abs_name e) TT) _ (invert_Abs e).
+    End unit.
+
     Definition Wf (Context : forall var, @Context base_type_code Name var) {t} (e : @expr base_type_code op Name t)
       := forall var, wf (Context var) empty e.
   End language.
 End Named.
 
+Global Arguments wff_gen {_ _ _ _ _} quantify ctx {t} _.
+Global Arguments wff_unit {_ _ _ _} ctx {t} _.
+Global Arguments wf_unit {_ _ _ _} ctx {t} _.
 Global Arguments wff {_ _ _ _ _} ctx {t} _.
 Global Arguments wf {_ _ _ _ _} ctx {t} _.
 Global Arguments Wf {_ _ _} Context {t} _.