diff --git a/src/haz3lcore/derivation/DrvElab.re b/src/haz3lcore/derivation/DrvElab.re
index b0d5dd9ae9..f131b23cce 100644
--- a/src/haz3lcore/derivation/DrvElab.re
+++ b/src/haz3lcore/derivation/DrvElab.re
@@ -60,6 +60,7 @@ and elab_prop: Drv.Prop.t => t =
           |> List.concat
           |> List.fold_left(cons_ctx, []),
         )
+      | Abbr(_) => Hole(Drv.Prop.show(prop))
       | Parens(p) => IdTagged.term_of(elab_prop(p))
       };
     {...prop, term};
@@ -146,6 +147,7 @@ and elab_exp: Drv.Exp.t => t =
         };
       | Roll => hole
       | Unroll => hole
+      | Abbr(_) => hole
       | Parens(e) => IdTagged.term_of(elab_exp(e))
       };
     {...exp, term};
diff --git a/src/haz3lcore/derivation/DrvInfo.re b/src/haz3lcore/derivation/DrvInfo.re
index 27bf5d6f7f..b7e11db2cd 100644
--- a/src/haz3lcore/derivation/DrvInfo.re
+++ b/src/haz3lcore/derivation/DrvInfo.re
@@ -24,12 +24,23 @@ type jdmt = {
   status: status_common,
 };
 
+[@deriving (show({with_path: false}), sexp, yojson)]
+type error_prop =
+  | BadToken(Token.t)
+  | MultiHole
+  | NotAllowTuple;
+
+[@deriving (show({with_path: false}), sexp, yojson)]
+type status_prop =
+  | NotInHole(ok_common)
+  | InHole(error_prop);
+
 [@deriving (show({with_path: false}), sexp, yojson)]
 type prop = {
   term: Drv.Prop.t,
   cls: Cls.t,
   ancestors,
-  status: status_common,
+  status: status_prop,
 };
 
 [@deriving (show({with_path: false}), sexp, yojson)]
@@ -109,7 +120,7 @@ type t =
 [@deriving (show({with_path: false}), sexp, yojson)]
 type error =
   | Jdmt(error_common)
-  | Prop(error_common)
+  | Prop(error_prop)
   | Exp(error_exp)
   | Pat(error_pat)
   | Typ(error_common)
@@ -160,7 +171,7 @@ let error_of: t => option(error) =
 [@deriving (show({with_path: false}), sexp, yojson)]
 type status_drv =
   | Jdmt(status_common)
-  | Prop(status_common)
+  | Prop(status_prop)
   | Exp(status_exp)
   | Pat(status_pat)
   | Typ(status_common)
@@ -173,7 +184,7 @@ let status_jdmt = (jdmt: Drv.Jdmt.t): status_common =>
   | _ => NotInHole()
   };
 
-let status_prop = (prop: Drv.Prop.t): status_common =>
+let status_prop = (prop: Drv.Prop.t): status_prop =>
   switch (prop.term) {
   | Hole(Invalid(token)) => InHole(BadToken(token))
   | Hole(MultiHole(_)) => InHole(MultiHole)
diff --git a/src/haz3lcore/derivation/DrvTerm.re b/src/haz3lcore/derivation/DrvTerm.re
index bec207377c..08c36cd358 100644
--- a/src/haz3lcore/derivation/DrvTerm.re
+++ b/src/haz3lcore/derivation/DrvTerm.re
@@ -44,6 +44,7 @@ module Prop = {
     | Truth
     | Falsity
     | Tuple
+    | Abbr
     | Parens;
 
   include TermBase.Prop;
@@ -75,6 +76,7 @@ module Prop = {
     | Truth => Truth
     | Falsity => Falsity
     | Tuple(_) => Tuple
+    | Abbr(_) => Abbr
     | Parens(_) => Parens;
 };
 
@@ -107,6 +109,7 @@ module ALFA_Exp = {
     | Case
     | Roll
     | Unroll
+    | Abbr
     | Parens;
 
   include TermBase.ALFA_Exp;
@@ -153,6 +156,7 @@ module ALFA_Exp = {
     | Case(_) => Case
     | Roll => Roll
     | Unroll => Unroll
+    | Abbr(_) => Abbr
     | Parens(_) => Parens;
 };
 
diff --git a/src/haz3lcore/dynamics/Transition.re b/src/haz3lcore/dynamics/Transition.re
index 78b17f6507..b21d5965e7 100644
--- a/src/haz3lcore/dynamics/Transition.re
+++ b/src/haz3lcore/dynamics/Transition.re
@@ -157,6 +157,215 @@ module Transition = (EV: EV_MODE) => {
      if anything about the current node changes, if only its
      children change, we use rewrap */
 
+  // let req_drv_value =
+  //     (req, state, env, drv: Drv.t, rewrap: Drv.t => t): EV.result => {
+  //   let req_jdmt_value =
+  //       (jdmt: Drv.Jdmt.t, rewrap: Drv.Jdmt.t => t): EV.result => {
+  //     // let. _ = otherwise(env, jdmt |> rewrap);
+  //     // Constructor;
+  //     // let wrap_ctx = (term): EvalCtx.t => Term({term, ids: [rep_id(jdmt)]});
+  //     let (term, rewrap_: Drv.Jdmt.term => Drv.Jdmt.t) =
+  //       IdTagged.unwrap(jdmt);
+  //     let rewrap = term => term |> rewrap_ |> rewrap;
+  //     switch (term) {
+  //     | Hole(s) =>
+  //       let. _ = otherwise(env, Hole(s) |> rewrap);
+  //       Constructor;
+  //     | Val(e) =>
+  //       let. _ = otherwise(env, Fun.id)
+  //       and. e' =
+  //         req_value(
+  //           req(state, env),
+  //           Fun.id,
+  //           (Derivation(Exp(e)): term) |> IdTagged.fresh,
+  //         );
+  //       let e' =
+  //         switch (IdTagged.term_of(e')) {
+  //         | Derivation(Exp(e')) => e'
+  //         | _ => raise(EvaluatorError.Exception(InvalidBoxedIntLit(e')))
+  //         };
+  //       Step({
+  //         expr: Val(e') |> rewrap,
+  //         state_update,
+  //         kind: InvalidStep,
+  //         is_value: true,
+  //       });
+  //     | Eval(e1, e2) =>
+  //       let. _ = otherwise(env, Eval(e1, e2) |> rewrap);
+  //       Constructor;
+  //     | Entail(p1, p2) =>
+  //       let. _ = otherwise(env, Entail(p1, p2) |> rewrap);
+  //       Constructor;
+  //     };
+  //   }
+  //   and req_prop_value = (prop: Drv.Prop.t, rewrap): EV.result => {
+  //     let (term, rewrap_) = IdTagged.unwrap(prop);
+  //     let rewrap = term => term |> rewrap_ |> rewrap;
+  //     switch (term) {
+  //     | Hole(s) =>
+  //       let. _ = otherwise(env, Hole(s) |> rewrap);
+  //       Constructor;
+  //     | HasTy(e, t) =>
+  //       let. _ = otherwise(env, (e, t) => HasTy(e, t) |> rewrap);
+  //       and. e' =
+  //         req_value(
+  //           req(state, env),
+  //           Fun.id,
+  //           (Derivation(Exp(e)): term) |> IdTagged.fresh,
+  //         )
+  //       and. t' =
+  //         req_value(
+  //           req(state, env),
+  //           Fun.id,
+  //           (Derivation(Typ(t)): term) |> IdTagged.fresh,
+  //         );
+  //       let e' =
+  //         switch (IdTagged.term_of(e')) {
+  //         | Derivation(Exp(e')) => e'
+  //         | _ => raise(EvaluatorError.Exception(InvalidBoxedIntLit(e')))
+  //         };
+  //     | _ =>
+  //       let. _ = otherwise(env, prop |> rewrap);
+  //       Constructor;
+  //     };
+  //   }
+  //   and req_exp_value = (exp: Drv.Exp.t, rewrap): EV.result => {
+  //     let. _ = otherwise(env, exp |> rewrap);
+  //     Constructor;
+  //   };
+  //   switch (drv) {
+  //   | Jdmt(jdmt) => req_jdmt_value(jdmt, jdmt => Jdmt(jdmt) |> rewrap)
+  //   | Prop(prop) => req_prop_value(prop, prop => Prop(prop) |> rewrap)
+  //   | Exp(exp) => req_exp_value(exp, exp => Exp(exp) |> rewrap)
+  //   | Pat(_)
+  //   | Typ(_)
+  //   | TPat(_) =>
+  //     let. _ = otherwise(env, drv |> rewrap);
+  //     Constructor;
+  //   };
+  // };
+
+  let replace_drv_abbrs = (env, d: t): t => {
+    let rec go_jdmt = jdmt => {
+      let (term, rewrap) = Drv.Jdmt.unwrap(jdmt);
+      let term: Drv.Jdmt.term =
+        switch (term) {
+        | Hole(s) => Hole(s)
+        | Val(e) => Val(go_exp(e))
+        | Eval(e1, e2) => Eval(e1, e2)
+        | Entail(p1, p2) => Entail(p1, p2)
+        };
+      term |> rewrap;
+    }
+    and go_prop = prop => {
+      let (term, rewrap) = Drv.Prop.unwrap(prop);
+      let term: Drv.Prop.term =
+        switch (term) {
+        | Hole(s) => Hole(s)
+        | HasTy(e, t) => HasTy(go_exp(e), t)
+        | Syn(e, t) => Syn(go_exp(e), t)
+        | Ana(e, t) => Ana(go_exp(e), t)
+        | Var(x) => Var(x)
+        | And(p1, p2) => And(go_prop(p1), go_prop(p2))
+        | Or(p1, p2) => Or(go_prop(p1), go_prop(p2))
+        | Impl(p1, p2) => Impl(go_prop(p1), go_prop(p2))
+        | Truth => Truth
+        | Falsity => Falsity
+        | Tuple(ps) => Tuple(List.map(go_prop, ps))
+        | Abbr(p) =>
+          let (let+) = (x, f) =>
+            switch (x) {
+            | Ok(x) => f(x)
+            | Error(s) => (Hole(Invalid(s)): Drv.Prop.term)
+            };
+          let+ p =
+            switch (IdTagged.term_of(p)) {
+            | Var(x) => Ok(x)
+            | _ => Error("Pat Not Var")
+            };
+          let+ d =
+            switch (ClosureEnvironment.lookup(env, p)) {
+            | Some(d) => Ok(d)
+            | None => Error("Pat Not Found")
+            };
+          let+ e =
+            switch (DHExp.term_of(d)) {
+            | Derivation(Prop(e)) => Ok(e)
+            | _ => Error("Pat Not Prop type")
+            };
+          e |> IdTagged.unwrap |> fst;
+        | Parens(p) => Parens(go_prop(p))
+        };
+      term |> rewrap;
+    }
+    and go_exp = exp => {
+      let (term, rewrap) = Drv.Exp.unwrap(exp);
+      let term: Drv.Exp.term =
+        switch (term) {
+        | Hole(s) => Hole(s)
+        | NumLit(n) => NumLit(n)
+        | Neg(e) => Neg(go_exp(e))
+        | Plus(e1, e2) => Plus(go_exp(e1), go_exp(e2))
+        | Minus(e1, e2) => Minus(go_exp(e1), go_exp(e2))
+        | Times(e1, e2) => Times(go_exp(e1), go_exp(e2))
+        | Gt(e1, e2) => Gt(go_exp(e1), go_exp(e2))
+        | Lt(e1, e2) => Lt(go_exp(e1), go_exp(e2))
+        | Eq(e1, e2) => Eq(go_exp(e1), go_exp(e2))
+        | True => True
+        | False => False
+        | If(e1, e2, e3) => If(go_exp(e1), go_exp(e2), go_exp(e3))
+        | Var(x) => Var(x)
+        | Let(x, e1, e2) => Let(x, go_exp(e1), go_exp(e2))
+        | Fix(x, e) => Fix(x, go_exp(e))
+        | Fun(x, e) => Fun(x, go_exp(e))
+        | Ap(e1, e2) => Ap(go_exp(e1), go_exp(e2))
+        | Pair(e1, e2) => Pair(go_exp(e1), go_exp(e2))
+        | Triv => Triv
+        | PrjL(e) => PrjL(go_exp(e))
+        | PrjR(e) => PrjR(go_exp(e))
+        | InjL => InjL
+        | InjR => InjR
+        | Case(e1, x, e2, y, e3) =>
+          Case(go_exp(e1), x, go_exp(e2), y, go_exp(e3))
+        | Roll => Roll
+        | Unroll => Unroll
+        | Abbr(p) =>
+          let (let+) = (x, f) =>
+            switch (x) {
+            | Ok(x) => f(x)
+            | Error(s) => (Hole(Invalid(s)): Drv.Exp.term)
+            };
+          let+ p =
+            switch (IdTagged.term_of(p)) {
+            | Var(x) => Ok(x)
+            | _ => Error("Pat Not Var")
+            };
+          let+ d =
+            switch (ClosureEnvironment.lookup(env, p)) {
+            | Some(d) => Ok(d)
+            | None => Error("Pat Not Found")
+            };
+          let+ e =
+            switch (DHExp.term_of(d)) {
+            | Derivation(Exp(e)) => Ok(e)
+            | _ => Error("Pat Not ALFA_Exp type")
+            };
+          e |> IdTagged.unwrap |> fst;
+        | Parens(e) => Parens(go_exp(e))
+        };
+      term |> rewrap;
+    };
+    let (term, rewrap) = IdTagged.unwrap(d);
+    let term: term =
+      switch (term) {
+      | Derivation(Jdmt(jdmt)) => Derivation(Jdmt(go_jdmt(jdmt)))
+      | Derivation(Prop(prop)) => Derivation(Prop(go_prop(prop)))
+      | Derivation(Exp(exp)) => Derivation(Exp(go_exp(exp)))
+      | _ => term
+      };
+    term |> rewrap;
+  };
+
   let transition = (req, state, env, d): 'a => {
     // Split DHExp into term and id information
     let (term, rewrap) = DHExp.unwrap(d);
@@ -343,23 +552,6 @@ module Transition = (EV: EV_MODE) => {
           d2,
         );
       switch (DHExp.term_of(d1')) {
-      // | Constructor(ctr, ty)
-      //     when
-      //       ctr
-      //       |> BuiltinsDerivation.to_term
-      //       |> Option.is_some
-      //       && Typ.matched_arrow([], ty)
-      //       |> snd
-      //       |> Typ.term_of == Typ.Prop =>
-      //   let term = ctr |> BuiltinsDerivation.to_term |> Option.get;
-      //   let expr = BuiltinsDerivation.transit(term, Some(d2'));
-      //   Step({
-      //     expr,
-      //     state_update,
-      //     // TODO(zhiyao): add new kind
-      //     kind: BuiltinAp(ctr),
-      //     is_value: false // Not necessarily a value because of InvalidOperations
-      //   });
       | Constructor(_) => Constructor
       | Fun(dp, d3, Some(env'), _) =>
         let.match env'' = (env', matches(dp, d2'));
@@ -459,32 +651,22 @@ module Transition = (EV: EV_MODE) => {
     | Deferral(_) =>
       let. _ = otherwise(env, d);
       Indet;
-    // | Constructor(ctr, ty)
-    //     when
-    //       ctr
-    //       |> BuiltinsDerivation.to_term
-    //       |> Option.is_some
-    //       && ty
-    //       |> Typ.term_of == Typ.Prop =>
-    //   let. _ = otherwise(env, d);
-    //   let term = ctr |> BuiltinsDerivation.to_term |> Option.get;
-    //   let expr = BuiltinsDerivation.transit(term, None);
-    //   Step({
-    //     expr,
-    //     state_update,
-    //     // TODO(zhiyao): add new kind
-    //     kind: BuiltinAp(ctr),
-    //     is_value: false // Not necessarily a value because of InvalidOperations
-    //   });
     | Bool(_)
     | Int(_)
     | Float(_)
     | String(_)
-    | Derivation(_)
     | Constructor(_)
     | BuiltinFun(_) =>
       let. _ = otherwise(env, d);
       Constructor;
+    | Derivation(_) =>
+      let. _ = otherwise(env, d);
+      Step({
+        expr: replace_drv_abbrs(env, d),
+        state_update,
+        kind: InvalidStep,
+        is_value: true,
+      });
     | If(c, d1, d2) =>
       let. _ = otherwise(env, c => If(c, d1, d2) |> rewrap)
       and. c' =
diff --git a/src/haz3lcore/lang/Form.re b/src/haz3lcore/lang/Form.re
index 10fd53fc5d..0fe7fc48d9 100644
--- a/src/haz3lcore/lang/Form.re
+++ b/src/haz3lcore/lang/Form.re
@@ -235,7 +235,15 @@ let atomic_forms: list((string, (string => bool, list(Mold.t)))) = [
   ("string", (is_string, [mk_op(Exp, []), mk_op(Pat, [])])),
   (
     "int_lit",
-    (is_int, [mk_op(Exp, []), mk_op(Pat, []), mk_op(Drv(Typ), [])]),
+    (
+      is_int,
+      [
+        mk_op(Exp, []),
+        mk_op(Pat, []),
+        mk_op(Drv(Exp), []),
+        mk_op(Drv(Typ), []),
+      ],
+    ),
   ),
   ("float_lit", (is_float, [mk_op(Exp, []), mk_op(Pat, [])])),
   ("bool_lit", (is_bool, [mk_op(Exp, []), mk_op(Pat, [])])),
@@ -365,12 +373,20 @@ let forms: list((string, t)) = [
   ),
   ("if_", mk(ds, ["if", "then", "else"], mk_pre(P.if_, Exp, [Exp, Exp]))),
   // Drv
-  ("of_alfa_typ", mk(ds, ["of_Typ", "end"], mk_op(Exp, [Drv(Typ)]))),
-  ("of_alfa_exp", mk(ds, ["of_Exp", "end"], mk_op(Exp, [Drv(Exp)]))),
-  ("of_alfa_pat", mk(ds, ["of_Pat", "end"], mk_op(Exp, [Drv(Pat)]))),
-  ("of_alfa_tpat", mk(ds, ["of_TPat", "end"], mk_op(Exp, [Drv(TPat)]))),
-  ("of_prop", mk(ds, ["of_Prop", "end"], mk_op(Exp, [Drv(Prop)]))),
-  ("of_jdmt", mk(ds, ["of_Jdmt", "end"], mk_op(Exp, [Drv(Jdmt)]))),
+  // ("of_alfa_typ", mk(ds, ["of_Typ", "end"], mk_op(Exp, [Drv(Typ)]))),
+  // ("of_alfa_exp", mk(ds, ["of_Exp", "end"], mk_op(Exp, [Drv(Exp)]))),
+  // ("of_alfa_pat", mk(ds, ["of_Pat", "end"], mk_op(Exp, [Drv(Pat)]))),
+  // ("of_alfa_tpat", mk(ds, ["of_TPat", "end"], mk_op(Exp, [Drv(TPat)]))),
+  // ("of_prop", mk(ds, ["of_Prop", "end"], mk_op(Exp, [Drv(Prop)]))),
+  // ("of_jdmt", mk(ds, ["of_Jdmt", "end"], mk_op(Exp, [Drv(Jdmt)]))),
+  (
+    "prop_alias",
+    mk(ds, ["prop", "=", "in"], mk_pre(P.let_, Exp, [Pat, Drv(Prop)])),
+  ),
+  (
+    "alfa_alias",
+    mk(ds, ["alfa", "=", "in"], mk_pre(P.let_, Exp, [Pat, Drv(Exp)])),
+  ),
   ("fake_val", mk(ds, ["val", "in"], mk_pre(P.filter, Exp, [Exp]))),
   ("fake_entail", mk(ds, ["entail", "in"], mk_pre(P.filter, Exp, [Exp]))),
   ("val", mk(ii, ["val", "end"], mk_op(Drv(Jdmt), [Drv(Exp)]))),
@@ -420,6 +436,7 @@ let forms: list((string, t)) = [
   ("impl", mk_infix("==>", Drv(Prop), P.ann)),
   ("cons", mk_infix(",", Drv(Prop), P.comma)),
   ("parens_prop", mk(ii, ["(", ")"], mk_op(Drv(Prop), [Drv(Prop)]))),
+  ("abbr_prop", mk(ii, ["{", "}"], mk_op(Drv(Prop), [Pat]))),
   // Drv(Exp)
   ("exp_neg", mk(ds, ["-"], mk_pre(P.neg, Drv(Exp), []))),
   ("exp_plus", mk_infix("+", Drv(Exp), P.plus)),
@@ -469,6 +486,7 @@ let forms: list((string, t)) = [
     ),
   ),
   ("exp_parens", mk(ii, ["(", ")"], mk_op(Drv(Exp), [Drv(Exp)]))),
+  ("abbr_exp", mk(ii, ["{", "}"], mk_op(Drv(Exp), [Pat]))),
   // Drv(Pat)
   (
     "pat_cast",
diff --git a/src/haz3lcore/statics/MakeTerm.re b/src/haz3lcore/statics/MakeTerm.re
index 5a0edcebc2..2d91cd67fa 100644
--- a/src/haz3lcore/statics/MakeTerm.re
+++ b/src/haz3lcore/statics/MakeTerm.re
@@ -224,6 +224,7 @@ and prop_term: unsorted => (Drv.Prop.term, list(Id.t)) = {
     }
   | Op(([(_id, (["(", ")"], [Drv(Prop(body))]))], [])) =>
     ret(Parens(body))
+  | Op(([(_id, (["{", "}"], [Pat(var)]))], [])) => ret(Abbr(var))
   | Pre(([(_id, ([t1, t2], [Drv(Exp(l))]))], []), Drv(Typ(r))) as tm =>
     switch (t1, t2) {
     | ("hasty", ":") => ret(HasTy(l, r))
@@ -271,6 +272,7 @@ and alfa_exp_term: unsorted => (Drv.Exp.term, list(Id.t)) = {
     }
   | Op(([(_id, (["(", ")"], [Drv(Exp(body))]))], [])) =>
     ret(Parens(body))
+  | Op(([(_id, (["{", "}"], [Pat(var)]))], [])) => ret(Abbr(var))
   | Pre(([(_id, t)], []), Drv(Exp(r))) as tm =>
     switch (t) {
     | (["-"], []) => ret(Neg(r))
@@ -426,13 +428,6 @@ and exp_term: unsorted => (UExp.term, list(Id.t)) = {
           Match(scrut, rules),
           ids,
         )
-      | (["of_Typ", "end"], [Drv(Typ(ty))]) => ret(Derivation(Typ(ty)))
-      | (["of_Exp", "end"], [Drv(Exp(e))]) => ret(Derivation(Exp(e)))
-      | (["of_Pat", "end"], [Drv(Pat(p))]) => ret(Derivation(Pat(p)))
-      | (["of_TPat", "end"], [Drv(TPat(tp))]) =>
-        ret(Derivation(TPat(tp)))
-      | (["of_Prop", "end"], [Drv(Prop(p))]) => ret(Derivation(Prop(p)))
-      | (["of_Jdmt", "end"], [Drv(Jdmt(j))]) => ret(Derivation(Jdmt(j)))
       | ([t], []) when t != " " && !Form.is_explicit_hole(t) =>
         ret(Invalid(t))
       | _ => ret(hole(tm))
@@ -461,6 +456,10 @@ and exp_term: unsorted => (UExp.term, list(Id.t)) = {
           Filter(Filter({act: (Step, All), pat: filter}), r)
         | (["type", "=", "in"], [TPat(tpat), Typ(def)]) =>
           TyAlias(tpat, def, r)
+        | (["prop", "=", "in"], [Pat(pat), Drv(Prop(def))]) =>
+          Let(pat, UExp.Derivation(Prop(def)) |> UExp.fresh, r)
+        | (["alfa", "=", "in"], [Pat(pat), Drv(Exp(def))]) =>
+          Let(pat, UExp.Derivation(Exp(def)) |> UExp.fresh, r)
         | (["if", "then", "else"], [Exp(cond), Exp(conseq)]) =>
           If(cond, conseq, r)
         | _ => hole(tm)
diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re
index 81e1af7b62..fb50b93046 100644
--- a/src/haz3lcore/statics/Statics.re
+++ b/src/haz3lcore/statics/Statics.re
@@ -153,7 +153,10 @@ let rec any_to_info_map =
       CoCtx.empty,
       utyp_to_info_map(~ctx, ~ancestors, ty, m) |> snd,
     )
-  | Drv(drv) => (CoCtx.empty, m |> drv_to_info_map(drv, ~ancestors) |> snd)
+  | Drv(drv) => (
+      CoCtx.empty,
+      m |> drv_to_info_map(drv, ~ancestors, ~ctx) |> snd,
+    )
   | Rul(_)
   | Nul ()
   | Any () => (CoCtx.empty, m)
@@ -167,7 +170,8 @@ and multi = (~ctx, ~ancestors, m, tms) =>
     ([], m),
     tms,
   )
-and drv_to_info_map = (drv: Drv.t, m: Map.t, ~ancestors): (DrvInfo.t, Map.t) => {
+and drv_to_info_map =
+    (drv: Drv.t, m: Map.t, ~ctx, ~ancestors): (DrvInfo.t, Map.t) => {
   let add = (drv, info, m) => (
     info,
     add_info(Drv.of_id(drv), InfoDrv(info), m),
@@ -179,28 +183,61 @@ and drv_to_info_map = (drv: Drv.t, m: Map.t, ~ancestors): (DrvInfo.t, Map.t) =>
       | Hole(_) => m
       | Val(e) => m |> go_exp'(e) |> snd
       | Eval(e1, e2) => m |> go_exp'(e1) |> snd |> go_exp'(e2) |> snd
-      | Entail(p1, p2) => m |> go_prop(p1) |> snd |> go_prop(p2) |> snd
+      | Entail(p1, p2) =>
+        m
+        |> go_prop(p1, ~can_tuple=true)
+        |> snd
+        |> go_prop(p2, ~can_tuple=false)
+        |> snd
       };
     add(Jdmt(jdmt), info, m);
   }
-  and go_prop = (prop: Drv.Prop.t, m) => {
-    let info: DrvInfo.t = Prop(DrvInfo.derived_prop(prop, ~ancestors));
-    let m =
-      switch (prop.term) {
-      | Hole(_) => m
-      | HasTy(e, t)
-      | Syn(e, t)
-      | Ana(e, t) => m |> go_exp'(e) |> snd |> go_typ(t) |> snd
-      | Var(_) => m
-      | And(p1, p2)
-      | Or(p1, p2)
-      | Impl(p1, p2) => m |> go_prop(p1) |> snd |> go_prop(p2) |> snd
-      | Truth
-      | Falsity => m
-      | Tuple(ps) => List.fold_left((m, p) => m |> go_prop(p) |> snd, m, ps)
-      | Parens(p) => m |> go_prop(p) |> snd
-      };
-    add(Prop(prop), info, m);
+  and go_prop = (prop: Drv.Prop.t, m, ~can_tuple: bool) => {
+    let info = DrvInfo.derived_prop(prop, ~ancestors);
+    let add' = add(Prop(prop), Prop(info));
+    // let m =
+    switch (prop.term) {
+    | Hole(_) => m |> add'
+    | HasTy(e, t)
+    | Syn(e, t)
+    | Ana(e, t) => m |> go_exp'(e) |> snd |> go_typ(t) |> snd |> add'
+    | Var(_) => m |> add'
+    | And(p1, p2)
+    | Or(p1, p2)
+    | Impl(p1, p2) =>
+      m
+      |> go_prop(p1, ~can_tuple=false)
+      |> snd
+      |> go_prop(p2, ~can_tuple=false)
+      |> snd
+      |> add'
+
+    | Truth
+    | Falsity => m |> add'
+    | Tuple(_) when !can_tuple =>
+      m |> add(Prop(prop), Prop({...info, status: InHole(NotAllowTuple)}))
+    | Tuple(ps) =>
+      List.fold_left(
+        (m, p) => m |> go_prop(p, ~can_tuple=false) |> snd,
+        m,
+        ps,
+      )
+      |> add'
+    | Abbr(p) =>
+      m
+      |> upat_to_info_map(
+           ~is_synswitch=false,
+           ~co_ctx=CoCtx.empty,
+           ~ctx,
+           ~ancestors,
+           ~mode=Mode.Ana(Derivation(DrvTyp.Prop) |> Typ.fresh),
+           p,
+         )
+      |> snd
+      |> add'
+    | Parens(p) => m |> go_prop(p, ~can_tuple) |> snd |> add'
+    };
+    // add(Prop(prop), info, m);
   }
   and go_exp = (exp: Drv.Exp.t, m, ~left_ap: bool) => {
     let info = DrvInfo.derived_exp(exp, ~ancestors);
@@ -255,6 +292,18 @@ and drv_to_info_map = (drv: Drv.t, m: Map.t, ~ancestors): (DrvInfo.t, Map.t) =>
       let m = m |> go_exp'(e1) |> snd;
       let m = m |> go_pat(p2, ~expect=Ap_InjR) |> snd;
       m |> go_exp'(e2) |> snd |> add';
+    | Abbr(p) =>
+      m
+      |> upat_to_info_map(
+           ~is_synswitch=false,
+           ~co_ctx=CoCtx.empty,
+           ~ctx,
+           ~ancestors,
+           ~mode=Mode.Ana(Derivation(DrvTyp.Prop) |> Typ.fresh),
+           p,
+         )
+      |> snd
+      |> add'
     | Parens(e) => m |> go_exp(e, ~left_ap) |> snd |> add'
     };
   }
@@ -311,7 +360,7 @@ and drv_to_info_map = (drv: Drv.t, m: Map.t, ~ancestors): (DrvInfo.t, Map.t) =>
   };
   switch (drv) {
   | Jdmt(jdmt) => go_jdmt(jdmt, m)
-  | Prop(prop) => go_prop(prop, m)
+  | Prop(prop) => go_prop(prop, m, ~can_tuple=true)
   | Exp(exp) => go_exp(exp, m, ~left_ap=false)
   | Pat(pat) => go_pat(pat, m, ~expect=Var)
   | Typ(ty) => go_typ(ty, m)
@@ -384,7 +433,7 @@ and uexp_to_info_map =
   | Float(_) => atomic(Just(Float |> Typ.temp))
   | String(_) => atomic(Just(String |> Typ.temp))
   | Derivation(d) =>
-    let m = drv_to_info_map(d, m, ~ancestors) |> snd;
+    let m = drv_to_info_map(d, m, ~ancestors, ~ctx) |> snd;
     add(
       ~self=Just(Derivation(Drv.of_typ(d)) |> Typ.temp),
       ~co_ctx=CoCtx.empty,
diff --git a/src/haz3lcore/statics/TermBase.re b/src/haz3lcore/statics/TermBase.re
index 8d33ea37ba..2cafbe7f3b 100644
--- a/src/haz3lcore/statics/TermBase.re
+++ b/src/haz3lcore/statics/TermBase.re
@@ -62,7 +62,7 @@ module rec Any: {
       ~f_tpat: (TPat.t => TPat.t, TPat.t) => TPat.t=?,
       ~f_rul: (Rul.t => Rul.t, Rul.t) => Rul.t=?,
       ~f_any: (Any.t => Any.t, Any.t) => Any.t=?,
-      ~f_derivation: Drv.mapper=?,
+      ~f_drv: Drv.mapper=?,
       t
     ) =>
     t;
@@ -88,12 +88,14 @@ module rec Any: {
         ~f_tpat=continue,
         ~f_rul=continue,
         ~f_any=continue,
-        ~f_derivation=Drv.continue,
+        ~f_drv=Drv.drv_continue,
         x,
       ) => {
+    let pat_map_term =
+      Pat.map_term(~f_exp, ~f_pat, ~f_typ, ~f_tpat, ~f_rul, ~f_any);
     let rec_call = y =>
       switch (y) {
-      | Drv(x) => Drv(Drv.map_term(f_derivation, x))
+      | Drv(x) => Drv(Drv.map_term(~f_hazel_pat=pat_map_term, ~f_drv, x))
       | Exp(x) =>
         Exp(
           Exp.map_term(
@@ -103,12 +105,11 @@ module rec Any: {
             ~f_tpat,
             ~f_rul,
             ~f_any,
-            ~f_derivation,
+            ~f_drv,
             x,
           ),
         )
-      | Pat(x) =>
-        Pat(Pat.map_term(~f_exp, ~f_pat, ~f_typ, ~f_tpat, ~f_rul, ~f_any, x))
+      | Pat(x) => Pat(pat_map_term(x))
       | Typ(x) =>
         Typ(Typ.map_term(~f_exp, ~f_pat, ~f_typ, ~f_tpat, ~f_rul, ~f_any, x))
       | TPat(x) =>
@@ -219,7 +220,7 @@ and Exp: {
       ~f_tpat: (TPat.t => TPat.t, TPat.t) => TPat.t=?,
       ~f_rul: (Rul.t => Rul.t, Rul.t) => Rul.t=?,
       ~f_any: (Any.t => Any.t, Any.t) => Any.t=?,
-      ~f_derivation: Drv.mapper=?,
+      ~f_drv: Drv.mapper=?,
       t
     ) =>
     t;
@@ -285,19 +286,11 @@ and Exp: {
         ~f_tpat=continue,
         ~f_rul=continue,
         ~f_any=continue,
-        ~f_derivation=Drv.continue,
+        ~f_drv=Drv.drv_continue,
         x,
       ) => {
     let exp_map_term =
-      Exp.map_term(
-        ~f_exp,
-        ~f_pat,
-        ~f_typ,
-        ~f_tpat,
-        ~f_rul,
-        ~f_any,
-        ~f_derivation,
-      );
+      Exp.map_term(~f_exp, ~f_pat, ~f_typ, ~f_tpat, ~f_rul, ~f_any, ~f_drv);
     let pat_map_term =
       Pat.map_term(~f_exp, ~f_pat, ~f_typ, ~f_tpat, ~f_rul, ~f_any);
     let typ_map_term =
@@ -315,6 +308,7 @@ and Exp: {
         ~f_rul,
         ~f_any,
       );
+    let drv_map_term = Drv.map_term(~f_hazel_pat=pat_map_term, ~f_drv);
     let rec_call = ({term, _} as exp: t) => {
       ...exp,
       term:
@@ -369,7 +363,7 @@ and Exp: {
             ),
           )
         | Cast(e, t1, t2) => Cast(exp_map_term(e), t1, t2)
-        | Derivation(d) => Derivation(Drv.map_term(f_derivation, d))
+        | Derivation(e) => Derivation(drv_map_term(e))
         },
     };
     x |> f_exp(rec_call);
@@ -1228,9 +1222,9 @@ and Drv: {
     f_tpat: (ALFA_TPat.t => ALFA_TPat.t, ALFA_TPat.t) => ALFA_TPat.t,
   };
 
-  let continue: mapper;
+  let drv_continue: mapper;
 
-  let map_term: (mapper, t) => t;
+  let map_term: (~f_hazel_pat: Pat.t => Pat.t=?, ~f_drv: mapper=?, t) => t;
 
   let fast_equal: (t, t) => bool;
 } = {
@@ -1252,7 +1246,7 @@ and Drv: {
     f_tpat: (ALFA_TPat.t => ALFA_TPat.t, ALFA_TPat.t) => ALFA_TPat.t,
   };
 
-  let continue = {
+  let drv_continue = {
     f_jdmt: continue,
     f_prop: continue,
     f_exp: continue,
@@ -1261,30 +1255,43 @@ and Drv: {
     f_tpat: continue,
   };
 
-  let map_term: (mapper, t) => t =
-    ({f_jdmt, f_prop, f_exp, f_pat, f_typ, f_tpat}, x) => {
-      switch (x) {
-      | Jdmt(jdmt) =>
-        Jdmt(
-          Jdmt.map_term(
-            ~f_jdmt,
-            ~f_prop,
-            ~f_exp,
-            ~f_pat,
-            ~f_typ,
-            ~f_tpat,
-            jdmt,
-          ),
-        )
-      | Prop(prop) =>
-        Prop(Prop.map_term(~f_prop, ~f_exp, ~f_pat, ~f_typ, ~f_tpat, prop))
-      | Exp(exp) =>
-        Exp(ALFA_Exp.map_term(~f_exp, ~f_pat, ~f_typ, ~f_tpat, exp))
-      | Pat(pat) => Pat(ALFA_Pat.map_term(~f_pat, ~f_typ, ~f_tpat, pat))
-      | Typ(typ) => Typ(ALFA_Typ.map_term(~f_typ, ~f_tpat, typ))
-      | TPat(tpat) => TPat(ALFA_TPat.map_term(~f_tpat, tpat))
-      };
+  let map_term = (~f_hazel_pat=continue, ~f_drv=drv_continue, x: t) => {
+    let {f_jdmt, f_prop, f_exp, f_pat, f_typ, f_tpat} = f_drv;
+    switch (x) {
+    | Jdmt(jdmt) =>
+      Jdmt(
+        Jdmt.map_term(
+          ~f_hazel_pat,
+          ~f_jdmt,
+          ~f_prop,
+          ~f_exp,
+          ~f_pat,
+          ~f_typ,
+          ~f_tpat,
+          jdmt,
+        ),
+      )
+    | Prop(prop) =>
+      Prop(
+        Prop.map_term(
+          ~f_hazel_pat,
+          ~f_prop,
+          ~f_exp,
+          ~f_pat,
+          ~f_typ,
+          ~f_tpat,
+          prop,
+        ),
+      )
+    | Exp(exp) =>
+      Exp(
+        ALFA_Exp.map_term(~f_hazel_pat, ~f_exp, ~f_pat, ~f_typ, ~f_tpat, exp),
+      )
+    | Pat(pat) => Pat(ALFA_Pat.map_term(~f_pat, ~f_typ, ~f_tpat, pat))
+    | Typ(typ) => Typ(ALFA_Typ.map_term(~f_typ, ~f_tpat, typ))
+    | TPat(tpat) => TPat(ALFA_TPat.map_term(~f_tpat, tpat))
     };
+  };
 
   let fast_equal = (x, y) =>
     switch (x, y) {
@@ -1313,6 +1320,7 @@ and Jdmt: {
 
   let map_term:
     (
+      ~f_hazel_pat: Pat.t => Pat.t=?,
       ~f_jdmt: (Jdmt.t => Jdmt.t, Jdmt.t) => Jdmt.t=?,
       ~f_prop: (Prop.t => Prop.t, Prop.t) => Prop.t=?,
       ~f_exp: (ALFA_Exp.t => ALFA_Exp.t, ALFA_Exp.t) => ALFA_Exp.t=?,
@@ -1335,6 +1343,7 @@ and Jdmt: {
 
   let map_term =
       (
+        ~f_hazel_pat=continue,
         ~f_jdmt=continue,
         ~f_prop=continue,
         ~f_exp=continue,
@@ -1344,8 +1353,9 @@ and Jdmt: {
         x,
       ) => {
     let prop_map_term =
-      Prop.map_term(~f_prop, ~f_exp, ~f_pat, ~f_typ, ~f_tpat);
-    let exp_map_term = ALFA_Exp.map_term(~f_exp, ~f_pat, ~f_typ, ~f_tpat);
+      Prop.map_term(~f_hazel_pat, ~f_prop, ~f_exp, ~f_pat, ~f_typ, ~f_tpat);
+    let exp_map_term =
+      ALFA_Exp.map_term(~f_hazel_pat, ~f_exp, ~f_pat, ~f_typ, ~f_tpat);
     let rec_call = ({term, _} as exp: t) => {
       ...exp,
       term:
@@ -1386,11 +1396,13 @@ and Prop: {
     | Truth
     | Falsity
     | Tuple(list(t))
+    | Abbr(Pat.t)
     | Parens(t)
   and t = IdTagged.t(term);
 
   let map_term:
     (
+      ~f_hazel_pat: Pat.t => Pat.t=?,
       ~f_prop: (Prop.t => Prop.t, Prop.t) => Prop.t=?,
       ~f_exp: (ALFA_Exp.t => ALFA_Exp.t, ALFA_Exp.t) => ALFA_Exp.t=?,
       ~f_pat: (ALFA_Pat.t => ALFA_Pat.t, ALFA_Pat.t) => ALFA_Pat.t=?,
@@ -1415,11 +1427,13 @@ and Prop: {
     | Truth
     | Falsity
     | Tuple(list(t))
+    | Abbr(Pat.t)
     | Parens(t)
   and t = IdTagged.t(term);
 
   let map_term =
       (
+        ~f_hazel_pat=continue,
         ~f_prop=continue,
         ~f_exp=continue,
         ~f_pat=continue,
@@ -1427,7 +1441,8 @@ and Prop: {
         ~f_tpat=continue,
         x,
       ) => {
-    let exp_map_term = ALFA_Exp.map_term(~f_exp, ~f_pat, ~f_typ, ~f_tpat);
+    let exp_map_term =
+      ALFA_Exp.map_term(~f_hazel_pat, ~f_exp, ~f_pat, ~f_typ, ~f_tpat);
     let typ_map_term = ALFA_Typ.map_term(~f_typ, ~f_tpat);
     let prop_map_term =
       Prop.map_term(~f_prop, ~f_exp, ~f_pat, ~f_typ, ~f_tpat);
@@ -1446,6 +1461,7 @@ and Prop: {
         | Truth => Truth
         | Falsity => Falsity
         | Tuple(pl) => Tuple(List.map(prop_map_term, pl))
+        | Abbr(e) => Abbr(f_hazel_pat(e))
         | Parens(p) => Parens(prop_map_term(p))
         },
     };
@@ -1481,6 +1497,8 @@ and Prop: {
     | (Falsity, _) => false
     | (Tuple(pl1), Tuple(pl2)) => List.equal(Prop.fast_equal, pl1, pl2)
     | (Tuple(_), _) => false
+    | (Abbr(p1), Abbr(p2)) => Pat.fast_equal(p1, p2)
+    | (Abbr(_), _) => false
     | (Parens(p1), Parens(p2)) => Prop.fast_equal(p1, p2)
     | (Parens(_), _) => false
     };
@@ -1514,11 +1532,13 @@ and ALFA_Exp: {
     | Case(t, ALFA_Pat.t, t, ALFA_Pat.t, t)
     | Roll
     | Unroll
+    | Abbr(Pat.t)
     | Parens(t)
   and t = IdTagged.t(term);
 
   let map_term:
     (
+      ~f_hazel_pat: Pat.t => Pat.t=?,
       ~f_exp: (ALFA_Exp.t => ALFA_Exp.t, ALFA_Exp.t) => ALFA_Exp.t=?,
       ~f_pat: (ALFA_Pat.t => ALFA_Pat.t, ALFA_Pat.t) => ALFA_Pat.t=?,
       ~f_typ: (ALFA_Typ.t => ALFA_Typ.t, ALFA_Typ.t) => ALFA_Typ.t=?,
@@ -1527,10 +1547,6 @@ and ALFA_Exp: {
     ) =>
     t;
 
-  let subst: (t, Var.t, t) => t;
-
-  let subst_ty: (ALFA_Typ.t, Var.t, t) => t;
-
   let fast_equal: (t, t) => bool;
 } = {
   [@deriving (show({with_path: false}), sexp, yojson)]
@@ -1561,12 +1577,21 @@ and ALFA_Exp: {
     | Case(t, ALFA_Pat.t, t, ALFA_Pat.t, t)
     | Roll
     | Unroll
+    | Abbr(Pat.t)
     | Parens(t)
   and t = IdTagged.t(term);
 
   let map_term =
-      (~f_exp=continue, ~f_pat=continue, ~f_typ=continue, ~f_tpat=continue, x) => {
-    let exp_map_term = ALFA_Exp.map_term(~f_exp, ~f_pat, ~f_typ, ~f_tpat);
+      (
+        ~f_hazel_pat=continue,
+        ~f_exp=continue,
+        ~f_pat=continue,
+        ~f_typ=continue,
+        ~f_tpat=continue,
+        x,
+      ) => {
+    let exp_map_term =
+      ALFA_Exp.map_term(~f_hazel_pat, ~f_exp, ~f_pat, ~f_typ, ~f_tpat);
     let pat_map_term = ALFA_Pat.map_term(~f_pat, ~f_typ, ~f_tpat);
     let rec_call = ({term, _} as exp: t) => {
       ...exp,
@@ -1607,94 +1632,13 @@ and ALFA_Exp: {
           )
         | Roll => Roll
         | Unroll => Unroll
+        | Abbr(e) => Abbr(f_hazel_pat(e))
         | Parens(e) => Parens(exp_map_term(e))
         },
     };
     x |> f_exp(rec_call);
   };
 
-  let rec subst = (v, x, e) => {
-    let (term, rewrap) = IdTagged.unwrap(e);
-    let subst = subst(v, x);
-    let is_shadowed = p => ALFA_Pat.var_of_pat(p) == Some(x);
-    let subx = p => is_shadowed(p) ? Fun.id : subst;
-    switch (term) {
-    | Hole(_) => e
-    | NumLit(_) => e
-    | Neg(e) => Neg(subst(e)) |> rewrap
-    | Plus(e1, e2) => Plus(subst(e1), subst(e2)) |> rewrap
-    | Minus(e1, e2) => Minus(subst(e1), subst(e2)) |> rewrap
-    | Times(e1, e2) => Times(subst(e1), subst(e2)) |> rewrap
-    | Gt(e1, e2) => Gt(subst(e1), subst(e2)) |> rewrap
-    | Lt(e1, e2) => Lt(subst(e1), subst(e2)) |> rewrap
-    | Eq(e1, e2) => Eq(subst(e1), subst(e2)) |> rewrap
-    | True => e
-    | False => e
-    | If(e1, e2, e3) => If(subst(e1), subst(e2), subst(e3)) |> rewrap
-    | Var(x') => x' == x ? v : e
-    | Let(p, e1, e2) => Let(p, subst(e1), subx(p, e2)) |> rewrap
-    | Fix(p, e) => Fix(p, subx(p, e)) |> rewrap
-    | Fun(p, e) => Fun(p, subx(p, e)) |> rewrap
-    | Ap(e1, e2) => Ap(subst(e1), subst(e2)) |> rewrap
-    | Pair(e1, e2) => Pair(subst(e1), subst(e2)) |> rewrap
-    | Triv => e
-    | PrjL(e) => PrjL(subst(e)) |> rewrap
-    | PrjR(e) => PrjR(subst(e)) |> rewrap
-    | InjL => e
-    | InjR => e
-    | Case(e, p1, e1, p2, e2) =>
-      Case(subst(e), p1, subx(p1, e1), p2, subx(p2, e2)) |> rewrap
-    | Roll => e
-    | Unroll => e
-    | Parens(e) => Parens(subst(e)) |> rewrap
-    };
-  };
-
-  let rec subst_ty = (t, x, e) => {
-    let (term, rewrap) = IdTagged.unwrap(e);
-    let subst_ty = subst_ty(t, x);
-    let pat_subst_ty = ALFA_Pat.subst_ty(t, x);
-    switch (term) {
-    | Hole(_) => e
-    | NumLit(_) => e
-    | Neg(e) => Neg(subst_ty(e)) |> rewrap
-    | Plus(e1, e2) => Plus(subst_ty(e1), subst_ty(e2)) |> rewrap
-    | Minus(e1, e2) => Minus(subst_ty(e1), subst_ty(e2)) |> rewrap
-    | Times(e1, e2) => Times(subst_ty(e1), subst_ty(e2)) |> rewrap
-    | Gt(e1, e2) => Gt(subst_ty(e1), subst_ty(e2)) |> rewrap
-    | Lt(e1, e2) => Lt(subst_ty(e1), subst_ty(e2)) |> rewrap
-    | Eq(e1, e2) => Eq(subst_ty(e1), subst_ty(e2)) |> rewrap
-    | True => e
-    | False => e
-    | If(e1, e2, e3) =>
-      If(subst_ty(e1), subst_ty(e2), subst_ty(e3)) |> rewrap
-    | Var(_) => e
-    | Let(p, e1, e2) =>
-      Let(pat_subst_ty(p), subst_ty(e1), subst_ty(e2)) |> rewrap
-    | Fix(p, e) => Fix(pat_subst_ty(p), subst_ty(e)) |> rewrap
-    | Fun(p, e) => Fun(pat_subst_ty(p), subst_ty(e)) |> rewrap
-    | Ap(e1, e2) => Ap(subst_ty(e1), subst_ty(e2)) |> rewrap
-    | Pair(e1, e2) => Pair(subst_ty(e1), subst_ty(e2)) |> rewrap
-    | Triv => e
-    | PrjL(e) => PrjL(subst_ty(e)) |> rewrap
-    | PrjR(e) => PrjR(subst_ty(e)) |> rewrap
-    | InjL => e
-    | InjR => e
-    | Case(e, p1, e1, p2, e2) =>
-      Case(
-        subst_ty(e),
-        pat_subst_ty(p1),
-        subst_ty(e1),
-        pat_subst_ty(p2),
-        subst_ty(e2),
-      )
-      |> rewrap
-    | Roll => e
-    | Unroll => e
-    | Parens(e) => Parens(subst_ty(e)) |> rewrap
-    };
-  };
-
   let fast_equal = (x, y) =>
     switch (x |> IdTagged.term_of, y |> IdTagged.term_of) {
     | (Hole(_), _) => false
@@ -1769,6 +1713,8 @@ and ALFA_Exp: {
     | (Roll, _) => false
     | (Unroll, Unroll) => true
     | (Unroll, _) => false
+    | (Abbr(p1), Abbr(p2)) => Pat.fast_equal(p1, p2)
+    | (Abbr(_), _) => false
     | (Parens(e1), Parens(e2)) => ALFA_Exp.fast_equal(e1, e2)
     | (Parens(_), _) => false
     };
@@ -1795,10 +1741,6 @@ and ALFA_Pat: {
     ) =>
     t;
 
-  let var_of_pat: t => option(Var.t);
-
-  let subst_ty: (ALFA_Typ.t, Var.t, t) => t;
-
   let fast_equal: (t, t) => bool;
 } = {
   [@deriving (show({with_path: false}), sexp, yojson)]
@@ -1833,34 +1775,6 @@ and ALFA_Pat: {
     x |> f_pat(rec_call);
   };
 
-  let var_of_pat = x =>
-    switch (x |> IdTagged.term_of) {
-    | Hole(_) => None
-    | Var(v) => Some(v)
-    | Cast(p, _) => ALFA_Pat.var_of_pat(p)
-    | InjL => None
-    | InjR => None
-    | Ap(_) => None
-    | Pair(_) => None
-    | Parens(p) => ALFA_Pat.var_of_pat(p)
-    };
-
-  let rec subst_ty = (t, x, p) => {
-    let (term, rewrap) = IdTagged.unwrap(p);
-    let subst_ty = subst_ty(t, x);
-    switch (term) {
-    | Hole(_) => p
-    | Var(_) => p
-    | Cast(p, t') =>
-      Cast(subst_ty(p), ALFA_Typ.subst_ty(t, x, t')) |> rewrap
-    | InjL => p
-    | InjR => p
-    | Ap(t1, t2) => Ap(subst_ty(t1), subst_ty(t2)) |> rewrap
-    | Pair(t1, t2) => Pair(subst_ty(t1), subst_ty(t2)) |> rewrap
-    | Parens(p) => Parens(subst_ty(p)) |> rewrap
-    };
-  };
-
   let fast_equal = (x, y) =>
     switch (x |> IdTagged.term_of, y |> IdTagged.term_of) {
     | (Hole(_), _) => false
@@ -1906,8 +1820,6 @@ and ALFA_Typ: {
     ) =>
     t;
 
-  let subst_ty: (ALFA_Typ.t, Var.t, t) => t;
-
   let fast_equal: (t, t) => bool;
 } = {
   [@deriving (show({with_path: false}), sexp, yojson)]
@@ -1946,25 +1858,6 @@ and ALFA_Typ: {
     x |> f_typ(rec_call);
   };
 
-  let rec subst_ty = (t, x, e) => {
-    let (term, rewrap) = IdTagged.unwrap(e);
-    let subst_ty = subst_ty(t, x);
-    let is_shadowed = p => ALFA_TPat.var_of_tpat(p) == Some(x);
-    let subx = p => is_shadowed(p) ? Fun.id : subst_ty;
-    switch (term) {
-    | Hole(_) => e
-    | Num => e
-    | Bool => e
-    | Arrow(t1, t2) => Arrow(subst_ty(t1), subst_ty(t2)) |> rewrap
-    | Prod(t1, t2) => Prod(subst_ty(t1), subst_ty(t2)) |> rewrap
-    | Unit => e
-    | Sum(t1, t2) => Sum(subst_ty(t1), subst_ty(t2)) |> rewrap
-    | Var(x') => x' == x ? t : e
-    | Rec(tp, t) => Rec(tp, subx(tp, t)) |> rewrap
-    | Parens(t) => Parens(subst_ty(t)) |> rewrap
-    };
-  };
-
   let fast_equal = (x, y) =>
     switch (x |> IdTagged.term_of, y |> IdTagged.term_of) {
     | (Hole(_), _) => false
@@ -2003,8 +1896,6 @@ and ALFA_TPat: {
     (~f_tpat: (ALFA_TPat.t => ALFA_TPat.t, ALFA_TPat.t) => ALFA_TPat.t=?, t) =>
     t;
 
-  let var_of_tpat: t => option(Var.t);
-
   let fast_equal: (t, t) => bool;
 } = {
   [@deriving (show({with_path: false}), sexp, yojson)]
@@ -2025,12 +1916,6 @@ and ALFA_TPat: {
     x |> f_tpat(rec_call);
   };
 
-  let var_of_tpat = x =>
-    switch (x |> IdTagged.term_of) {
-    | Hole(_) => None
-    | Var(v) => Some(v)
-    };
-
   let fast_equal = (x, y) =>
     switch (x |> IdTagged.term_of, y |> IdTagged.term_of) {
     | (Hole(_), _) => false
diff --git a/src/haz3lweb/view/CursorInspector.re b/src/haz3lweb/view/CursorInspector.re
index 2a0dfd48ea..e70d69b4d6 100644
--- a/src/haz3lweb/view/CursorInspector.re
+++ b/src/haz3lweb/view/CursorInspector.re
@@ -191,6 +191,12 @@ let drv_view = (status: DrvInfo.t) => {
     | Typ(BadToken(token))
     | TPat(BadToken(token)) =>
       div_err([text(Printf.sprintf("\"%s\" isn't a valid token", token))])
+    | Jdmt(MultiHole)
+    | Prop(MultiHole)
+    | Exp(MultiHole)
+    | Pat(MultiHole)
+    | Typ(MultiHole)
+    | TPat(MultiHole) => div_err([text("Expecting operator or delimiter")])
     | Pat(Expect(expect)) =>
       let expect =
         switch (expect) {
@@ -204,14 +210,10 @@ let drv_view = (status: DrvInfo.t) => {
         | InjR => "A Right Injection pattern"
         };
       div_err([text("Expected " ++ expect)]);
-    | Jdmt(MultiHole)
-    | Prop(MultiHole)
-    | Exp(MultiHole)
-    | Pat(MultiHole)
-    | Typ(MultiHole)
-    | TPat(MultiHole) => div_err([text("Expecting operator or delimiter")])
     | Exp(NotAllowSingle) =>
       div_err([text("Expected a compound expression of this")])
+    | Prop(NotAllowTuple) =>
+      div_err([text("Expected no comma in this position")])
     }
   };
 };
diff --git a/src/haz3lweb/view/exercise/ProofView.re b/src/haz3lweb/view/exercise/ProofView.re
index f246912e17..670b361f21 100644
--- a/src/haz3lweb/view/exercise/ProofView.re
+++ b/src/haz3lweb/view/exercise/ProofView.re
@@ -445,32 +445,29 @@ let proof_view =
       ],
     );
 
-  // let prelude_view =
-  //   editor_view(
-  //     Proof(Prelude),
-  //     ~editor=eds.prelude,
-  //     ~di=stitched_dynamics.prelude,
-  //     ~caption=
-  //       Cell.caption(
-  //         "Prelude",
-  //         ~rest=settings.instructor_mode ? "" : " (Read-Only)",
-  //       ),
-  //     ~sort=Exp,
-  //     ~footer=[],
-  //   );
-
-  // let setup_view =
-  //   editor_view(
-  //     Proof(Setup),
-  //     ~editor=eds.setup,
-  //     ~di=stitched_dynamics.setup,
-  //     ~caption=Cell.caption("Setup"),
-  //     ~sort=Exp,
-  //     ~footer=[],
-  //   );
-
-  [
-    // prelude_view, setup_view,
-    derivation_view,
-  ];
+  let prelude_view =
+    editor_view(
+      Proof(Prelude),
+      ~editor=eds.prelude,
+      ~di=stitched_dynamics.prelude,
+      ~caption=
+        Cell.caption(
+          "Prelude",
+          ~rest=settings.instructor_mode ? "" : " (Read-Only)",
+        ),
+      ~sort=Exp,
+      ~footer=[],
+    );
+
+  let setup_view =
+    editor_view(
+      Proof(Setup),
+      ~editor=eds.setup,
+      ~di=stitched_dynamics.setup,
+      ~caption=Cell.caption("Setup"),
+      ~sort=Exp,
+      ~footer=[],
+    );
+
+  [prelude_view, setup_view, derivation_view];
 };