diff --git a/src/haz3lcore/assistant/AssistantForms.re b/src/haz3lcore/assistant/AssistantForms.re
index 4330d6ac0a..110a9a1087 100644
--- a/src/haz3lcore/assistant/AssistantForms.re
+++ b/src/haz3lcore/assistant/AssistantForms.re
@@ -34,7 +34,12 @@ module Typ = {
     ("test" ++ leading_expander, Prod([]) |> Typ.fresh),
     ("type" ++ leading_expander, unk),
     ("val" ++ leading_expander, unk),
-    ("entail" ++ leading_expander, unk),
+    ("entail_hastype" ++ leading_expander, unk),
+    // ("entail_ana" ++ leading_expander, unk),
+    // ("entail_syn" ++ leading_expander, unk),
+    ("of_alfa_exp" ++ leading_expander, unk),
+    ("of_prop" ++ leading_expander, unk),
+    ("of_ctxt" ++ leading_expander, unk),
     ("eval" ++ leading_expander, unk),
   ];
 
diff --git a/src/haz3lcore/derivation/DrvElab.re b/src/haz3lcore/derivation/DrvElab.re
index fad3ddaaa9..99328d527c 100644
--- a/src/haz3lcore/derivation/DrvElab.re
+++ b/src/haz3lcore/derivation/DrvElab.re
@@ -6,15 +6,10 @@ let to_list = d =>
   | _ => [d]
   };
 
-let to_ctx = d =>
-  switch (DrvSyntax.term_of(d)) {
-  | Ctx(_) => d
-  | _ => Ctx([d]) |> DrvSyntax.fresh
-  };
-
 let rec elaborate: Drv.t => t =
   fun
   | Jdmt(jdmt) => elab_jdmt(jdmt)
+  | Ctxt(ctxt) => elab_ctxt(ctxt)
   | Prop(prop) => elab_prop(prop)
   | Exp(exp) => elab_exp(exp)
   | Pat(pat) => elab_pat(pat)
@@ -27,16 +22,43 @@ and elab_jdmt: Drv.Jdmt.t => t =
       | Hole(s) => Hole(TermBase.TypeHole.show(s))
       | Val(e) => Val(elab_exp(e))
       | Eval(e1, e2) => Eval(elab_exp(e1), elab_exp(e2))
-      | Entail(p1, p2) => Entail(elab_prop(p1) |> to_ctx, elab_prop(p2))
+      | Entail(ctx, p) => Entail(elab_ctxt(ctx), elab_prop(p))
       };
     {...jdmt, term};
   }
+and elab_ctxt: Drv.Ctxt.t => t =
+  ctxt => {
+    let rec prop_term_of: Drv.Prop.t => Drv.Prop.term =
+      pat =>
+        switch (pat.term) {
+        | Parens(p) => prop_term_of(p)
+        | p => p
+        };
+    let term: term =
+      switch (ctxt.term) {
+      | Hole(s) => Hole(TermBase.TypeHole.show(s))
+      | Ctxt(p) =>
+        switch (prop_term_of(p)) {
+        | Tuple(ps) =>
+          Ctx(
+            ps
+            |> List.map(elab_prop)
+            |> List.map(to_list)
+            |> List.concat
+            |> List.fold_left(cons_ctx, []),
+          )
+        | _ => Ctx([elab_prop(p)])
+        }
+      };
+    {...ctxt, term};
+  }
 and elab_prop: Drv.Prop.t => t =
   prop => {
+    let hole: term = Hole(Drv.Prop.show(prop));
     let term: term =
       switch (prop.term) {
       | Hole(s) => Hole(TermBase.TypeHole.show(s))
-      | HasTy(e, t) => HasTy(elab_exp(e), elab_typ(t))
+      | HasType(e, t) => HasType(elab_exp(e), elab_typ(t))
       | Syn(e, t) => Syn(elab_exp(e), elab_typ(t))
       | Ana(e, t) => Ana(elab_exp(e), elab_typ(t))
       | Var(x) => Atom(x)
@@ -45,15 +67,8 @@ and elab_prop: Drv.Prop.t => t =
       | Impl(p1, p2) => Impl(elab_prop(p1), elab_prop(p2))
       | Truth => Truth
       | Falsity => Falsity
-      | Tuple(ps) =>
-        Ctx(
-          ps
-          |> List.map(elab_prop)
-          |> List.map(to_list)
-          |> List.concat
-          |> List.fold_left(cons_ctx, []),
-        )
-      | Abbr(_) => Hole(Drv.Prop.show(prop))
+      | Tuple(_) => hole
+      | Abbr(_) => hole
       | Parens(p) => IdTagged.term_of(elab_prop(p))
       };
     {...prop, term};
diff --git a/src/haz3lcore/derivation/DrvInfo.re b/src/haz3lcore/derivation/DrvInfo.re
index b7e11db2cd..45fa90680b 100644
--- a/src/haz3lcore/derivation/DrvInfo.re
+++ b/src/haz3lcore/derivation/DrvInfo.re
@@ -24,6 +24,14 @@ type jdmt = {
   status: status_common,
 };
 
+[@deriving (show({with_path: false}), sexp, yojson)]
+type ctxt = {
+  term: Drv.Ctxt.t,
+  cls: Cls.t,
+  ancestors,
+  status: status_common,
+};
+
 [@deriving (show({with_path: false}), sexp, yojson)]
 type error_prop =
   | BadToken(Token.t)
@@ -111,6 +119,7 @@ type tpat = {
 [@deriving (show({with_path: false}), sexp, yojson)]
 type t =
   | Jdmt(jdmt)
+  | Ctxt(ctxt)
   | Prop(prop)
   | Exp(exp)
   | Pat(pat)
@@ -120,6 +129,7 @@ type t =
 [@deriving (show({with_path: false}), sexp, yojson)]
 type error =
   | Jdmt(error_common)
+  | Ctxt(error_common)
   | Prop(error_prop)
   | Exp(error_exp)
   | Pat(error_pat)
@@ -129,6 +139,7 @@ type error =
 let sort_of: t => Sort.DrvSort.t =
   fun
   | Jdmt(_) => Jdmt
+  | Ctxt(_) => Ctxt
   | Prop(_) => Prop
   | Exp(_) => Exp
   | Pat(_) => Pat
@@ -138,6 +149,7 @@ let sort_of: t => Sort.DrvSort.t =
 let cls_of: t => Cls.t =
   fun
   | Jdmt(jdmt) => jdmt.cls
+  | Ctxt(ctxt) => ctxt.cls
   | Prop(prop) => prop.cls
   | Exp(exp) => exp.cls
   | Pat(pat) => pat.cls
@@ -147,6 +159,7 @@ let cls_of: t => Cls.t =
 let id_of: t => Id.t =
   fun
   | Jdmt(jdmt) => Drv.Jdmt.rep_id(jdmt.term)
+  | Ctxt(ctxt) => Drv.Ctxt.rep_id(ctxt.term)
   | Prop(prop) => Drv.Prop.rep_id(prop.term)
   | Exp(exp) => Drv.Exp.rep_id(exp.term)
   | Pat(pat) => Drv.Pat.rep_id(pat.term)
@@ -156,12 +169,14 @@ let id_of: t => Id.t =
 let error_of: t => option(error) =
   fun
   | Jdmt({status: NotInHole(_), _})
+  | Ctxt({status: NotInHole(_), _})
   | Prop({status: NotInHole(_), _})
   | Exp({status: NotInHole(_), _})
   | Pat({status: NotInHole(_), _})
   | Typ({status: NotInHole(_), _})
   | TPat({status: NotInHole(_), _}) => None
   | Jdmt({status: InHole(err), _}) => Some(Jdmt(err))
+  | Ctxt({status: InHole(err), _}) => Some(Ctxt(err))
   | Prop({status: InHole(err), _}) => Some(Prop(err))
   | Exp({status: InHole(err), _}) => Some(Exp(err))
   | Pat({status: InHole(err), _}) => Some(Pat(err))
@@ -171,6 +186,7 @@ let error_of: t => option(error) =
 [@deriving (show({with_path: false}), sexp, yojson)]
 type status_drv =
   | Jdmt(status_common)
+  | Ctxt(status_common)
   | Prop(status_prop)
   | Exp(status_exp)
   | Pat(status_pat)
@@ -184,6 +200,13 @@ let status_jdmt = (jdmt: Drv.Jdmt.t): status_common =>
   | _ => NotInHole()
   };
 
+let status_ctxt = (ctxt: Drv.Ctxt.t): status_common =>
+  switch (ctxt.term) {
+  | Hole(Invalid(token)) => InHole(BadToken(token))
+  | Hole(MultiHole(_)) => InHole(MultiHole)
+  | _ => NotInHole()
+  };
+
 let status_prop = (prop: Drv.Prop.t): status_prop =>
   switch (prop.term) {
   | Hole(Invalid(token)) => InHole(BadToken(token))
@@ -222,6 +245,7 @@ let status_tpat = (tpat: Drv.TPat.t): status_common =>
 let status_drv = (drv: Drv.t): status_drv =>
   switch (drv) {
   | Jdmt(term) => Jdmt(status_jdmt(term))
+  | Ctxt(term) => Ctxt(status_ctxt(term))
   | Prop(term) => Prop(status_prop(term))
   | Exp(term) => Exp(status_exp(term))
   | Pat(term) => Pat(status_pat(term))
@@ -232,12 +256,14 @@ let status_drv = (drv: Drv.t): status_drv =>
 let is_error = (ci: t): bool => {
   switch (ci) {
   | Jdmt({status: InHole(_), _})
+  | Ctxt({status: InHole(_), _})
   | Prop({status: InHole(_), _})
   | Exp({status: InHole(_), _})
   | Pat({status: InHole(_), _})
   | Typ({status: InHole(_), _})
   | TPat({status: InHole(_), _}) => true
   | Jdmt({status: NotInHole(_), _})
+  | Ctxt({status: NotInHole(_), _})
   | Prop({status: NotInHole(_), _})
   | Exp({status: NotInHole(_), _})
   | Pat({status: NotInHole(_), _})
@@ -249,6 +275,7 @@ let is_error = (ci: t): bool => {
 let ancestors_of: t => ancestors =
   fun
   | Jdmt({ancestors, _})
+  | Ctxt({ancestors, _})
   | Prop({ancestors, _})
   | Exp({ancestors, _})
   | Pat({ancestors, _})
@@ -261,6 +288,12 @@ let derived_jdmt = (jdmt: Drv.Jdmt.t, ~ancestors): jdmt => {
   {term: jdmt, cls, status, ancestors};
 };
 
+let derived_ctxt = (ctxt: Drv.Ctxt.t, ~ancestors): ctxt => {
+  let cls = Cls.Drv(Ctxt(Drv.Ctxt.cls_of_term(ctxt.term)));
+  let status = status_ctxt(ctxt);
+  {term: ctxt, cls, status, ancestors};
+};
+
 let derived_prop = (prop: Drv.Prop.t, ~ancestors): prop => {
   let cls = Cls.Drv(Prop(Drv.Prop.cls_of_term(prop.term)));
   let status = status_prop(prop);
@@ -294,6 +327,7 @@ let derived_tpat = (tpat: Drv.TPat.t, ~ancestors): tpat => {
 let derived_drv = (drv: Drv.t, ~ancestors): t => {
   switch (drv) {
   | Jdmt(jdmt) => Jdmt(derived_jdmt(jdmt, ~ancestors))
+  | Ctxt(ctxt) => Ctxt(derived_ctxt(ctxt, ~ancestors))
   | Prop(prop) => Prop(derived_prop(prop, ~ancestors))
   | Exp(exp) => Exp(derived_exp(exp, ~ancestors))
   | Pat(pat) => Pat(derived_pat(pat, ~ancestors))
diff --git a/src/haz3lcore/derivation/DrvSyntax.re b/src/haz3lcore/derivation/DrvSyntax.re
index d680c7ed18..508d939e61 100644
--- a/src/haz3lcore/derivation/DrvSyntax.re
+++ b/src/haz3lcore/derivation/DrvSyntax.re
@@ -24,7 +24,7 @@ type term =
   | Eval(t, t)
   | Entail(t, t)
   // Proposition
-  | HasTy(t, t)
+  | HasType(t, t)
   | Syn(t, t)
   | Ana(t, t)
   | Atom(string)
@@ -93,7 +93,7 @@ type cls =
   | Val
   | Eval
   | Entail
-  | HasTy
+  | HasType
   | Syn
   | Ana
   | Atom
@@ -152,7 +152,7 @@ let precedence: t => int =
     | Val(_) => P.filter
     | Eval(_) => P.filter
     | Entail(_) => P.filter
-    | HasTy(_) => P.semi
+    | HasType(_) => P.semi
     | Syn(_) => P.semi
     | Ana(_) => P.semi
     | Atom(_) => P.max
@@ -293,7 +293,7 @@ let rec repr = (p: int, prop: t): list(string) => {
     | Unroll(a) => repr_aba_tight(["unroll(", ")"], [a])
     | TPat(x) => x |> mk
     | Pat(x) => x |> mk
-    | HasTy(a, b) => repr_binop(":", a, b)
+    | HasType(a, b) => repr_binop(":", a, b)
     | Syn(a, b) => repr_binop("⇒", a, b)
     | Ana(a, b) => repr_binop("⇐", a, b)
     }
@@ -395,8 +395,8 @@ let rec eq: (t, t) => bool =
     | (TPat(_), _) => false
     | (Pat(a), Pat(b)) => String.equal(a, b)
     | (Pat(_), _) => false
-    | (HasTy(a1, a2), HasTy(b1, b2)) => eq(a1, b1) && eq(a2, b2)
-    | (HasTy(_), _) => false
+    | (HasType(a1, a2), HasType(b1, b2)) => eq(a1, b1) && eq(a2, b2)
+    | (HasType(_), _) => false
     | (Syn(a1, a2), Syn(b1, b2)) => eq(a1, b1) && eq(a2, b2)
     | (Syn(_), _) => false
     | (Ana(a1, a2), Ana(b1, b2)) => eq(a1, b1) && eq(a2, b2)
@@ -486,7 +486,7 @@ let rec subst: (t, string, t) => t =
     | TPat(_)
     | Pat(_)
     // Proposition
-    | HasTy(_)
+    | HasType(_)
     | Syn(_)
     | Ana(_) => e
     // Logic
@@ -571,7 +571,7 @@ let rec subst_ty: (t, string, t) => t =
     | TPat(_)
     | Pat(_) => e
     // Proposition
-    | HasTy(_)
+    | HasType(_)
     | Syn(_)
     | Ana(_) => e
     // Logic
diff --git a/src/haz3lcore/derivation/DrvTerm.re b/src/haz3lcore/derivation/DrvTerm.re
index 0305ea1ac8..4a07ef32fa 100644
--- a/src/haz3lcore/derivation/DrvTerm.re
+++ b/src/haz3lcore/derivation/DrvTerm.re
@@ -30,11 +30,39 @@ module Jdmt = {
     | Entail(_) => Entail;
 };
 
+module Ctxt = {
+  [@deriving (show({with_path: false}), sexp, yojson)]
+  type cls =
+    | Hole
+    | Ctxt;
+
+  include TermBase.Ctxt;
+
+  let hole = (tms: list(TermBase.Any.t)): term =>
+    Hole(List.is_empty(tms) ? EmptyHole : MultiHole(tms));
+
+  let rep_id = ({ids, _}: t) => {
+    assert(ids != []);
+    List.hd(ids);
+  };
+
+  let term_of: t => term = IdTagged.term_of;
+
+  let unwrap: t => (term, term => t) = IdTagged.unwrap;
+
+  let fresh: term => t = IdTagged.fresh;
+
+  let cls_of_term: term => cls =
+    fun
+    | Hole(_) => Hole
+    | Ctxt(_) => Ctxt;
+};
+
 module Prop = {
   [@deriving (show({with_path: false}), sexp, yojson)]
   type cls =
     | Hole
-    | HasTy
+    | HasType
     | Syn
     | Ana
     | Var
@@ -66,7 +94,7 @@ module Prop = {
   let cls_of_term: term => cls =
     fun
     | Hole(_) => Hole
-    | HasTy(_) => HasTy
+    | HasType(_) => HasType
     | Syn(_) => Syn
     | Ana(_) => Ana
     | Var(_) => Var
@@ -276,6 +304,7 @@ module Drv = {
   [@deriving (show({with_path: false}), sexp, yojson)]
   type cls =
     | Jdmt(Jdmt.cls)
+    | Ctxt(Ctxt.cls)
     | Prop(Prop.cls)
     | Exp(ALFA_Exp.cls)
     | Pat(ALFA_Pat.cls)
@@ -287,6 +316,7 @@ module Drv = {
   let sort_of: t => Sort.DrvSort.t =
     fun
     | Jdmt(_) => Jdmt
+    | Ctxt(_) => Ctxt
     | Prop(_) => Prop
     | Exp(_) => Exp
     | Pat(_) => Pat
@@ -296,6 +326,7 @@ module Drv = {
   let rep_id: t => Id.t =
     fun
     | Jdmt(jdmt) => Jdmt.rep_id(jdmt)
+    | Ctxt(ctxt) => Ctxt.rep_id(ctxt)
     | Prop(prop) => Prop.rep_id(prop)
     | Exp(exp) => ALFA_Exp.rep_id(exp)
     | Pat(pat) => ALFA_Pat.rep_id(pat)
@@ -305,6 +336,7 @@ module Drv = {
   let of_id: t => list(Id.t) =
     fun
     | Jdmt(jdmt) => jdmt.ids
+    | Ctxt(ctxt) => ctxt.ids
     | Prop(prop) => prop.ids
     | Exp(exp) => exp.ids
     | Pat(pat) => pat.ids
@@ -314,6 +346,7 @@ module Drv = {
   let cls_of: t => cls =
     fun
     | Jdmt(jdmt) => Jdmt(Jdmt.cls_of_term(jdmt.term))
+    | Ctxt(ctxt) => Ctxt(Ctxt.cls_of_term(ctxt.term))
     | Prop(prop) => Prop(Prop.cls_of_term(prop.term))
     | Exp(exp) => Exp(ALFA_Exp.cls_of_term(exp.term))
     | Pat(pat) => Pat(ALFA_Pat.cls_of_term(pat.term))
diff --git a/src/haz3lcore/derivation/RuleExample.re b/src/haz3lcore/derivation/RuleExample.re
index 7786441b0c..413600990a 100644
--- a/src/haz3lcore/derivation/RuleExample.re
+++ b/src/haz3lcore/derivation/RuleExample.re
@@ -27,10 +27,15 @@ let of_ghost: Rule.t => deduction(t) =
     let n2 = () => !Var("n₂");
     let gamma = () => !Var("Γ");
     let ctx = () => !Ctx([gamma()]);
-    let ctx_x = () => !Ctx([gamma(), !HasTy(!Var("x"), t1())]);
-    let ctx_y = () => !Ctx([gamma(), !HasTy(!Var("y"), t2())]);
+    let ctx_x = () => !Ctx([gamma(), !HasType(!Var("x"), t1())]);
+    let ctx_y = () => !Ctx([gamma(), !HasType(!Var("y"), t2())]);
     let ctx_xy = () =>
-      !Ctx([gamma(), !HasTy(!Var("y"), t2()), !HasTy(!Var("x"), t1())]);
+      !
+        Ctx([
+          gamma(),
+          !HasType(!Var("y"), t2()),
+          !HasType(!Var("x"), t1()),
+        ]);
     let ctx_a = () => !Ctx([gamma(), a()]);
     let ctx_b = () => !Ctx([gamma(), b()]);
     switch (rule) {
@@ -46,7 +51,7 @@ let of_ghost: Rule.t => deduction(t) =
       let concl = !Entail(ctx(), !Syn(n(), !Num));
       {concl, prems: []};
     | T_Num =>
-      let concl = !Entail(ctx(), !HasTy(n(), !Num));
+      let concl = !Entail(ctx(), !HasType(n(), !Num));
       {concl, prems: []};
     | V_Num =>
       let concl = !Val(n());
@@ -55,7 +60,7 @@ let of_ghost: Rule.t => deduction(t) =
       let concl = !Entail(ctx(), !Syn(!True, !Bool));
       {concl, prems: []};
     | T_True =>
-      let concl = !Entail(ctx(), !HasTy(!True, !Bool));
+      let concl = !Entail(ctx(), !HasType(!True, !Bool));
       {concl, prems: []};
     | V_True =>
       let concl = !Val(!True);
@@ -64,7 +69,7 @@ let of_ghost: Rule.t => deduction(t) =
       let concl = !Entail(ctx(), !Syn(!False, !Bool));
       {concl, prems: []};
     | T_False =>
-      let concl = !Entail(ctx(), !HasTy(!False, !Bool));
+      let concl = !Entail(ctx(), !HasType(!False, !Bool));
       {concl, prems: []};
     | V_False =>
       let concl = !Val(!False);
@@ -73,7 +78,7 @@ let of_ghost: Rule.t => deduction(t) =
       let concl = !Entail(ctx(), !Syn(!Triv, !Unit));
       {concl, prems: []};
     | T_Triv =>
-      let concl = !Entail(ctx(), !HasTy(!Triv, !Unit));
+      let concl = !Entail(ctx(), !HasType(!Triv, !Unit));
       {concl, prems: []};
     | V_Triv =>
       let concl = !Val(!Triv);
@@ -83,8 +88,8 @@ let of_ghost: Rule.t => deduction(t) =
       let concl = !Entail(ctx(), !Syn(!Neg(e()), !Num));
       {concl, prems};
     | T_Neg =>
-      let prems = [!Entail(ctx(), !HasTy(e(), !Num))];
-      let concl = !Entail(ctx(), !HasTy(!Neg(e()), !Num));
+      let prems = [!Entail(ctx(), !HasType(e(), !Num))];
+      let concl = !Entail(ctx(), !HasType(!Neg(e()), !Num));
       {concl, prems};
     | E_Neg =>
       let prems = [!Eval(e(), n1())];
@@ -99,10 +104,10 @@ let of_ghost: Rule.t => deduction(t) =
       {concl, prems};
     | T_Plus =>
       let prems = [
-        !Entail(ctx(), !HasTy(e1(), !Num)),
-        !Entail(ctx(), !HasTy(e2(), !Num)),
+        !Entail(ctx(), !HasType(e1(), !Num)),
+        !Entail(ctx(), !HasType(e2(), !Num)),
       ];
-      let concl = !Entail(ctx(), !HasTy(!Plus(e1(), e2()), !Num));
+      let concl = !Entail(ctx(), !HasType(!Plus(e1(), e2()), !Num));
       {concl, prems};
     | E_Plus =>
       let prems = [!Eval(e1(), n1()), !Eval(e2(), n2())];
@@ -117,10 +122,10 @@ let of_ghost: Rule.t => deduction(t) =
       {concl, prems};
     | T_Minus =>
       let prems = [
-        !Entail(ctx(), !HasTy(e1(), !Num)),
-        !Entail(ctx(), !HasTy(e2(), !Num)),
+        !Entail(ctx(), !HasType(e1(), !Num)),
+        !Entail(ctx(), !HasType(e2(), !Num)),
       ];
-      let concl = !Entail(ctx(), !HasTy(!Minus(e1(), e2()), !Num));
+      let concl = !Entail(ctx(), !HasType(!Minus(e1(), e2()), !Num));
       {concl, prems};
     | E_Minus =>
       let prems = [!Eval(e1(), n1()), !Eval(e2(), n2())];
@@ -135,10 +140,10 @@ let of_ghost: Rule.t => deduction(t) =
       {concl, prems};
     | T_Times =>
       let prems = [
-        !Entail(ctx(), !HasTy(e1(), !Num)),
-        !Entail(ctx(), !HasTy(e2(), !Num)),
+        !Entail(ctx(), !HasType(e1(), !Num)),
+        !Entail(ctx(), !HasType(e2(), !Num)),
       ];
-      let concl = !Entail(ctx(), !HasTy(!Times(e1(), e2()), !Num));
+      let concl = !Entail(ctx(), !HasType(!Times(e1(), e2()), !Num));
       {concl, prems};
     | E_Times =>
       let prems = [!Eval(e1(), n1()), !Eval(e2(), n2())];
@@ -153,10 +158,10 @@ let of_ghost: Rule.t => deduction(t) =
       {concl, prems};
     | T_Lt =>
       let prems = [
-        !Entail(ctx(), !HasTy(e1(), !Num)),
-        !Entail(ctx(), !HasTy(e2(), !Num)),
+        !Entail(ctx(), !HasType(e1(), !Num)),
+        !Entail(ctx(), !HasType(e2(), !Num)),
       ];
-      let concl = !Entail(ctx(), !HasTy(!Lt(e1(), e2()), !Bool));
+      let concl = !Entail(ctx(), !HasType(!Lt(e1(), e2()), !Bool));
       {concl, prems};
     | E_Lt_T =>
       let prems = [!Eval(e1(), n1()), !Eval(e2(), n2())];
@@ -175,10 +180,10 @@ let of_ghost: Rule.t => deduction(t) =
       {concl, prems};
     | T_Gt =>
       let prems = [
-        !Entail(ctx(), !HasTy(e1(), !Num)),
-        !Entail(ctx(), !HasTy(e2(), !Num)),
+        !Entail(ctx(), !HasType(e1(), !Num)),
+        !Entail(ctx(), !HasType(e2(), !Num)),
       ];
-      let concl = !Entail(ctx(), !HasTy(!Gt(e1(), e2()), !Bool));
+      let concl = !Entail(ctx(), !HasType(!Gt(e1(), e2()), !Bool));
       {concl, prems};
     | E_Gt_T =>
       let prems = [!Eval(e1(), n1()), !Eval(e2(), n2())];
@@ -197,10 +202,10 @@ let of_ghost: Rule.t => deduction(t) =
       {concl, prems};
     | T_Eq =>
       let prems = [
-        !Entail(ctx(), !HasTy(e1(), !Num)),
-        !Entail(ctx(), !HasTy(e2(), !Num)),
+        !Entail(ctx(), !HasType(e1(), !Num)),
+        !Entail(ctx(), !HasType(e2(), !Num)),
       ];
-      let concl = !Entail(ctx(), !HasTy(!Eq(e1(), e2()), !Bool));
+      let concl = !Entail(ctx(), !HasType(!Eq(e1(), e2()), !Bool));
       {concl, prems};
     | E_Eq_T =>
       let prems = [!Eval(e1(), n()), !Eval(e2(), n())];
@@ -228,11 +233,11 @@ let of_ghost: Rule.t => deduction(t) =
       {concl, prems};
     | T_If =>
       let prems = [
-        !Entail(ctx(), !HasTy(e1(), !Bool)),
-        !Entail(ctx(), !HasTy(e2(), t())),
-        !Entail(ctx(), !HasTy(e3(), t())),
+        !Entail(ctx(), !HasType(e1(), !Bool)),
+        !Entail(ctx(), !HasType(e2(), t())),
+        !Entail(ctx(), !HasType(e3(), t())),
       ];
-      let concl = !Entail(ctx(), !HasTy(!If(e1(), e2(), e3()), t()));
+      let concl = !Entail(ctx(), !HasType(!If(e1(), e2(), e3()), t()));
       {concl, prems};
     | E_If_T =>
       let prems = [!Eval(e1(), !True), !Eval(e2(), v2())];
@@ -244,11 +249,11 @@ let of_ghost: Rule.t => deduction(t) =
       {concl, prems};
     | S_Var =>
       let concl =
-        !Entail(!Ctx([ctx(), !HasTy(x(), t1())]), !Syn(x(), t1()));
+        !Entail(!Ctx([ctx(), !HasType(x(), t1())]), !Syn(x(), t1()));
       {concl, prems: []};
     | T_Var =>
       let concl =
-        !Entail(!Ctx([ctx(), !HasTy(x(), t1())]), !HasTy(x(), t1()));
+        !Entail(!Ctx([ctx(), !HasType(x(), t1())]), !HasType(x(), t1()));
       {concl, prems: []};
     | S_LetAnn =>
       let prems = [
@@ -268,11 +273,11 @@ let of_ghost: Rule.t => deduction(t) =
       {concl, prems};
     | T_LetAnn =>
       let prems = [
-        !Entail(ctx(), !HasTy(e1(), t1())),
-        !Entail(ctx_x(), !HasTy(e2(), t())),
+        !Entail(ctx(), !HasType(e1(), t1())),
+        !Entail(ctx_x(), !HasType(e2(), t())),
       ];
       let concl =
-        !Entail(ctx(), !HasTy(!LetAnn(xp(), t1(), e1(), e2()), t()));
+        !Entail(ctx(), !HasType(!LetAnn(xp(), t1(), e1(), e2()), t()));
       {concl, prems};
     | S_Let =>
       let prems = [
@@ -290,10 +295,10 @@ let of_ghost: Rule.t => deduction(t) =
       {concl, prems};
     | T_Let =>
       let prems = [
-        !Entail(ctx(), !HasTy(e1(), t1())),
-        !Entail(ctx_x(), !HasTy(e2(), t())),
+        !Entail(ctx(), !HasType(e1(), t1())),
+        !Entail(ctx_x(), !HasType(e2(), t())),
       ];
-      let concl = !Entail(ctx(), !HasTy(!Let(xp(), e1(), e2()), t()));
+      let concl = !Entail(ctx(), !HasType(!Let(xp(), e1(), e2()), t()));
       {concl, prems};
     | E_Let =>
       let prems = [!Eval(e1(), v1()), !Eval(ex(), v2())];
@@ -318,12 +323,12 @@ let of_ghost: Rule.t => deduction(t) =
           );
       {concl, prems};
     | T_FunAnn =>
-      let prems = [!Entail(ctx_x(), !HasTy(e1(), t2()))];
+      let prems = [!Entail(ctx_x(), !HasType(e1(), t2()))];
       let concl =
         !
           Entail(
             ctx(),
-            !HasTy(!FunAnn(xp(), t1(), e1()), !Arrow(t1(), t2())),
+            !HasType(!FunAnn(xp(), t1(), e1()), !Arrow(t1(), t2())),
           );
       {concl, prems};
     | A_Fun =>
@@ -332,20 +337,20 @@ let of_ghost: Rule.t => deduction(t) =
         !Entail(ctx(), !Ana(!Fun(xp(), e1()), !Arrow(t1(), t2())));
       {concl, prems};
     | T_Fun =>
-      let prems = [!Entail(ctx_x(), !HasTy(e1(), t2()))];
+      let prems = [!Entail(ctx_x(), !HasType(e1(), t2()))];
       let concl =
-        !Entail(ctx(), !HasTy(!Fun(xp(), e1()), !Arrow(t1(), t2())));
+        !Entail(ctx(), !HasType(!Fun(xp(), e1()), !Arrow(t1(), t2())));
       {concl, prems};
     | V_Fun =>
       let concl = !Val(!Fun(xp(), e()));
       {concl, prems: []};
     | T_Fix =>
-      let prems = [!Entail(ctx_x(), !HasTy(e(), t1()))];
-      let concl = !Entail(ctx(), !HasTy(!Fix(xp(), e()), t1()));
+      let prems = [!Entail(ctx_x(), !HasType(e(), t1()))];
+      let concl = !Entail(ctx(), !HasType(!Fix(xp(), e()), t1()));
       {concl, prems};
     | T_FixAnn =>
-      let prems = [!Entail(ctx_x(), !HasTy(e(), t1()))];
-      let concl = !Entail(ctx(), !HasTy(!FixAnn(xp(), t1(), e()), t1()));
+      let prems = [!Entail(ctx_x(), !HasType(e(), t1()))];
+      let concl = !Entail(ctx(), !HasType(!FixAnn(xp(), t1(), e()), t1()));
       {concl, prems};
     | E_Fix =>
       let prems = [!Eval(!Var("[fix x → e₁/x]e₁"), v())];
@@ -360,10 +365,10 @@ let of_ghost: Rule.t => deduction(t) =
       {concl, prems};
     | T_Ap =>
       let prems = [
-        !Entail(ctx(), !HasTy(e1(), !Arrow(t1(), t2()))),
-        !Entail(ctx(), !HasTy(e2(), t1())),
+        !Entail(ctx(), !HasType(e1(), !Arrow(t1(), t2()))),
+        !Entail(ctx(), !HasType(e2(), t1())),
       ];
-      let concl = !Entail(ctx(), !HasTy(!Ap(e1(), e2()), t2()));
+      let concl = !Entail(ctx(), !HasType(!Ap(e1(), e2()), t2()));
       {concl, prems};
     | E_Ap =>
       let prems = [
@@ -391,11 +396,11 @@ let of_ghost: Rule.t => deduction(t) =
       {concl, prems};
     | T_Pair =>
       let prems = [
-        !Entail(ctx(), !HasTy(e1(), t1())),
-        !Entail(ctx(), !HasTy(e2(), t2())),
+        !Entail(ctx(), !HasType(e1(), t1())),
+        !Entail(ctx(), !HasType(e2(), t2())),
       ];
       let concl =
-        !Entail(ctx(), !HasTy(!Pair(e1(), e2()), !Prod(t1(), t2())));
+        !Entail(ctx(), !HasType(!Pair(e1(), e2()), !Prod(t1(), t2())));
       {concl, prems};
     | E_Pair =>
       let prems = [!Eval(e1(), v1()), !Eval(e2(), v2())];
@@ -423,11 +428,11 @@ let of_ghost: Rule.t => deduction(t) =
       {concl, prems};
     | T_LetPair =>
       let prems = [
-        !Entail(ctx(), !HasTy(e1(), !Prod(t1(), t2()))),
-        !Entail(ctx_xy(), !HasTy(e2(), t())),
+        !Entail(ctx(), !HasType(e1(), !Prod(t1(), t2()))),
+        !Entail(ctx_xy(), !HasType(e2(), t())),
       ];
       let concl =
-        !Entail(ctx(), !HasTy(!LetPair(xp(), yp(), e1(), e2()), t()));
+        !Entail(ctx(), !HasType(!LetPair(xp(), yp(), e1(), e2()), t()));
       {concl, prems};
     | E_LetPair =>
       let prems = [
@@ -441,8 +446,8 @@ let of_ghost: Rule.t => deduction(t) =
       let concl = !Entail(ctx(), !Syn(!PrjL(e()), t1()));
       {concl, prems};
     | T_PrjL =>
-      let prems = [!Entail(ctx(), !HasTy(e(), !Prod(t1(), t2())))];
-      let concl = !Entail(ctx(), !HasTy(!PrjL(e()), t1()));
+      let prems = [!Entail(ctx(), !HasType(e(), !Prod(t1(), t2())))];
+      let concl = !Entail(ctx(), !HasType(!PrjL(e()), t1()));
       {concl, prems};
     | E_PrjL =>
       let prems = [!Eval(e(), !Pair(v1(), v2()))];
@@ -453,8 +458,8 @@ let of_ghost: Rule.t => deduction(t) =
       let concl = !Entail(ctx(), !Syn(!PrjR(e()), t2()));
       {concl, prems};
     | T_PrjR =>
-      let prems = [!Entail(ctx(), !HasTy(e(), !Prod(t1(), t2())))];
-      let concl = !Entail(ctx(), !HasTy(!PrjR(e()), t2()));
+      let prems = [!Entail(ctx(), !HasType(e(), !Prod(t1(), t2())))];
+      let concl = !Entail(ctx(), !HasType(!PrjR(e()), t2()));
       {concl, prems};
     | E_PrjR =>
       let prems = [!Eval(e(), !Pair(v1(), v2()))];
@@ -465,8 +470,8 @@ let of_ghost: Rule.t => deduction(t) =
       let concl = !Entail(ctx(), !Ana(!InjL(e()), !Sum(t1(), t2())));
       {concl, prems};
     | T_InjL =>
-      let prems = [!Entail(ctx(), !HasTy(e(), t1()))];
-      let concl = !Entail(ctx(), !HasTy(!InjL(e()), !Sum(t1(), t2())));
+      let prems = [!Entail(ctx(), !HasType(e(), t1()))];
+      let concl = !Entail(ctx(), !HasType(!InjL(e()), !Sum(t1(), t2())));
       {concl, prems};
     | E_InjL =>
       let prems = [!Eval(e(), v())];
@@ -481,8 +486,8 @@ let of_ghost: Rule.t => deduction(t) =
       let concl = !Entail(ctx(), !Ana(!InjR(e()), !Sum(t1(), t2())));
       {concl, prems};
     | T_InjR =>
-      let prems = [!Entail(ctx(), !HasTy(e(), t2()))];
-      let concl = !Entail(ctx(), !HasTy(!InjR(e()), !Sum(t1(), t2())));
+      let prems = [!Entail(ctx(), !HasType(e(), t2()))];
+      let concl = !Entail(ctx(), !HasType(!InjR(e()), !Sum(t1(), t2())));
       {concl, prems};
     | E_InjR =>
       let prems = [!Eval(e(), v())];
@@ -512,12 +517,12 @@ let of_ghost: Rule.t => deduction(t) =
       {concl, prems};
     | T_Case =>
       let prems = [
-        !Entail(ctx(), !HasTy(e(), !Sum(t1(), t2()))),
-        !Entail(ctx_x(), !HasTy(e1(), t())),
-        !Entail(ctx_y(), !HasTy(e2(), t())),
+        !Entail(ctx(), !HasType(e(), !Sum(t1(), t2()))),
+        !Entail(ctx_x(), !HasType(e1(), t())),
+        !Entail(ctx_y(), !HasType(e2(), t())),
       ];
       let concl =
-        !Entail(ctx(), !HasTy(!Case(e(), xp(), e1(), yp(), e2()), t()));
+        !Entail(ctx(), !HasType(!Case(e(), xp(), e1(), yp(), e2()), t()));
       {concl, prems};
     | E_Case_L =>
       let prems = [!Eval(e(), !InjL(v1())), !Eval(ex(), v())];
@@ -531,8 +536,8 @@ let of_ghost: Rule.t => deduction(t) =
       let concl = !Eval(!Case(e(), xp(), e1(), yp(), e2()), v());
       {concl, prems};
     | T_Roll =>
-      let prems = [!Entail(ctx(), !HasTy(e(), !Var("[rec a is t/a]t")))];
-      let concl = !Entail(ctx(), !HasTy(!Roll(e()), !Rec(a(), t())));
+      let prems = [!Entail(ctx(), !HasType(e(), !Var("[rec a is t/a]t")))];
+      let concl = !Entail(ctx(), !HasType(!Roll(e()), !Rec(a(), t())));
       {concl, prems};
     | E_Roll =>
       let prems = [!Eval(e(), v())];
@@ -543,9 +548,9 @@ let of_ghost: Rule.t => deduction(t) =
       let concl = !Val(!Roll(v()));
       {concl, prems};
     | T_Unroll =>
-      let prems = [!Entail(ctx(), !HasTy(e(), !Rec(a(), t())))];
+      let prems = [!Entail(ctx(), !HasType(e(), !Rec(a(), t())))];
       let concl =
-        !Entail(ctx(), !HasTy(!Unroll(e()), !Var("[rec a is t/a]t")));
+        !Entail(ctx(), !HasType(!Unroll(e()), !Var("[rec a is t/a]t")));
       {concl, prems};
     | E_Unroll =>
       let prems = [!Eval(e(), !Roll(v()))];
diff --git a/src/haz3lcore/derivation/RuleVerify.re b/src/haz3lcore/derivation/RuleVerify.re
index 8e35346ce4..20fd2236fb 100644
--- a/src/haz3lcore/derivation/RuleVerify.re
+++ b/src/haz3lcore/derivation/RuleVerify.re
@@ -202,7 +202,7 @@ type req('a) =
   | TPat: req(string)
   | Pat: req(string)
   // ALFA Proposition
-  | HasTy(req('a), req('b)): req(('a, 'b))
+  | HasType(req('a), req('b)): req(('a, 'b))
   | Syn(req('a), req('b)): req(('a, 'b))
   | Ana(req('a), req('b)): req(('a, 'b))
   // Logical Proposition
@@ -416,11 +416,11 @@ and unbox_self: type a. (DrvSyntax.t, req(a)) => result(a, failure) =
       Ok((a, b));
     | (Eq(_), _) => Error(FailUnbox(Eq, p))
     // ALFA proposition
-    | (HasTy(ra, rb), HasTy(a, b)) =>
+    | (HasType(ra, rb), HasType(a, b)) =>
       let$ a = unbox(a, ra);
       let$ b = unbox(b, rb);
       Ok((a, b));
-    | (HasTy(_), _) => Error(FailUnbox(HasTy, p))
+    | (HasType(_), _) => Error(FailUnbox(HasType, p))
     | (Syn(ra, rb), Syn(a, b)) =>
       let$ a = unbox(a, ra);
       let$ b = unbox(b, rb);
@@ -665,11 +665,11 @@ and unbox_with_ghost:
       Ok((a, b));
     | (Eq(_), _, _) => Error(FailUnbox(Eq, p))
     // ALFA proposition
-    | (HasTy(ra, rb), HasTy(a, b), HasTy(a', b')) =>
+    | (HasType(ra, rb), HasType(a, b), HasType(a', b')) =>
       let$ a = unbox(a, a', ra);
       let$ b = unbox(b, b', rb);
       Ok((a, b));
-    | (HasTy(_), _, _) => Error(FailUnbox(HasTy, p))
+    | (HasType(_), _, _) => Error(FailUnbox(HasType, p))
     | (Syn(ra, rb), Syn(a, b), Syn(a', b')) =>
       let$ a = unbox(a, a', ra);
       let$ b = unbox(b, b', rb);
@@ -789,21 +789,21 @@ and check: (t, operation) => result(bool, failure) =
     | ConsHasTy((pat, t), l) =>
       let$ l = unbox_list(l);
       let$ x = unbox_pat(pat);
-      let l = Ctx(cons_ctx(l, HasTy(x, t.self) |> temp)) |> temp;
+      let l = Ctx(cons_ctx(l, HasType(x, t.self) |> temp)) |> temp;
       Ok(eq(self, l));
     | ConsHasTy2((pat1, t1), (pat2, t2), l) =>
       let$ l = unbox_list(l);
       let$ x1 = unbox_pat(pat1);
       let$ x2 = unbox_pat(pat2);
-      let l = cons_ctx(l, HasTy(x1, t1.self) |> temp);
-      let l = Ctx(cons_ctx(l, HasTy(x2, t2.self) |> temp)) |> temp;
+      let l = cons_ctx(l, HasType(x1, t1.self) |> temp);
+      let l = Ctx(cons_ctx(l, HasType(x2, t2.self) |> temp)) |> temp;
       Ok(eq(self, l));
     | Mem(e) =>
       let$ l = unbox_list(p);
       Ok(mem_ctx(e.self, l));
     | MemHasTy(x, t) =>
       let$ l = unbox_list(p);
-      Ok(mem_ctx(HasTy(x.self, t.self) |> temp, l));
+      Ok(mem_ctx(HasType(x.self, t.self) |> temp, l));
     };
   };
 
@@ -837,7 +837,7 @@ let verify = (rule: Rule.t, prems: list(t), concl: t): result(unit, failure) =>
     let$ _ = concl >> Entail(__, Syn(NumLit, Num));
     Ok();
   | T_Num =>
-    let$ _ = concl >> Entail(__, HasTy(NumLit, Num));
+    let$ _ = concl >> Entail(__, HasType(NumLit, Num));
     Ok();
   | V_Num =>
     let$ _ = concl >> Val(NumLit);
@@ -846,7 +846,7 @@ let verify = (rule: Rule.t, prems: list(t), concl: t): result(unit, failure) =>
     let$ _ = concl >> Entail(__, Syn(True, Bool));
     Ok();
   | T_True =>
-    let$ _ = concl >> Entail(__, HasTy(True, Bool));
+    let$ _ = concl >> Entail(__, HasType(True, Bool));
     Ok();
   | V_True =>
     let$ _ = concl >> Val(True);
@@ -855,7 +855,7 @@ let verify = (rule: Rule.t, prems: list(t), concl: t): result(unit, failure) =>
     let$ _ = concl >> Entail(__, Syn(False, Bool));
     Ok();
   | T_False =>
-    let$ _ = concl >> Entail(__, HasTy(False, Bool));
+    let$ _ = concl >> Entail(__, HasType(False, Bool));
     Ok();
   | V_False =>
     let$ _ = concl >> Val(False);
@@ -864,7 +864,7 @@ let verify = (rule: Rule.t, prems: list(t), concl: t): result(unit, failure) =>
     let$ _ = concl >> Entail(__, Syn(Triv, Unit));
     Ok();
   | T_Triv =>
-    let$ _ = concl >> Entail(__, HasTy(Triv, Unit));
+    let$ _ = concl >> Entail(__, HasType(Triv, Unit));
     Ok();
   | V_Triv =>
     let$ _ = concl >> Val(Triv);
@@ -874,8 +874,8 @@ let verify = (rule: Rule.t, prems: list(t), concl: t): result(unit, failure) =>
     let$ _ = concl >> Entail(!ctx, Syn(Neg(!e), Num));
     Ok();
   | T_Neg =>
-    let$ (ctx, (e, _)) = prems(0) >> Entail(__, HasTy(__, Num));
-    let$ _ = concl >> Entail(!ctx, HasTy(Neg(!e), Num));
+    let$ (ctx, (e, _)) = prems(0) >> Entail(__, HasType(__, Num));
+    let$ _ = concl >> Entail(!ctx, HasType(Neg(!e), Num));
     Ok();
   | E_Neg =>
     let$ (e, v) = prems(0) >> Eval(__, __);
@@ -887,9 +887,9 @@ let verify = (rule: Rule.t, prems: list(t), concl: t): result(unit, failure) =>
     let$ _ = concl >> Entail(!ctx, Syn(Plus(!e1, !e2), Num));
     Ok();
   | T_Plus =>
-    let$ (ctx, (e1, _)) = prems(0) >> Entail(__, HasTy(__, Num));
-    let$ (_, (e2, _)) = prems(1) >> Entail(!ctx, HasTy(__, Num));
-    let$ _ = concl >> Entail(!ctx, HasTy(Plus(!e1, !e2), Num));
+    let$ (ctx, (e1, _)) = prems(0) >> Entail(__, HasType(__, Num));
+    let$ (_, (e2, _)) = prems(1) >> Entail(!ctx, HasType(__, Num));
+    let$ _ = concl >> Entail(!ctx, HasType(Plus(!e1, !e2), Num));
     Ok();
   | E_Plus =>
     let$ (e1, v1) = prems(0) >> Eval(__, __);
@@ -902,9 +902,9 @@ let verify = (rule: Rule.t, prems: list(t), concl: t): result(unit, failure) =>
     let$ _ = concl >> Entail(!ctx, Syn(Minus(!e1, !e2), Num));
     Ok();
   | T_Minus =>
-    let$ (ctx, (e1, _)) = prems(0) >> Entail(__, HasTy(__, Num));
-    let$ (_, (e2, _)) = prems(1) >> Entail(!ctx, HasTy(__, Num));
-    let$ _ = concl >> Entail(!ctx, HasTy(Minus(!e1, !e2), Num));
+    let$ (ctx, (e1, _)) = prems(0) >> Entail(__, HasType(__, Num));
+    let$ (_, (e2, _)) = prems(1) >> Entail(!ctx, HasType(__, Num));
+    let$ _ = concl >> Entail(!ctx, HasType(Minus(!e1, !e2), Num));
     Ok();
   | E_Minus =>
     let$ (e1, v1) = prems(0) >> Eval(__, __);
@@ -917,9 +917,9 @@ let verify = (rule: Rule.t, prems: list(t), concl: t): result(unit, failure) =>
     let$ _ = concl >> Entail(!ctx, Syn(Times(!e1, !e2), Num));
     Ok();
   | T_Times =>
-    let$ (ctx, (e1, _)) = prems(0) >> Entail(__, HasTy(__, Num));
-    let$ (_, (e2, _)) = prems(1) >> Entail(!ctx, HasTy(__, Num));
-    let$ _ = concl >> Entail(!ctx, HasTy(Times(!e1, !e2), Num));
+    let$ (ctx, (e1, _)) = prems(0) >> Entail(__, HasType(__, Num));
+    let$ (_, (e2, _)) = prems(1) >> Entail(!ctx, HasType(__, Num));
+    let$ _ = concl >> Entail(!ctx, HasType(Times(!e1, !e2), Num));
     Ok();
   | E_Times =>
     let$ (e1, v1) = prems(0) >> Eval(__, __);
@@ -932,9 +932,9 @@ let verify = (rule: Rule.t, prems: list(t), concl: t): result(unit, failure) =>
     let$ _ = concl >> Entail(!ctx, Syn(Lt(!e1, !e2), Bool));
     Ok();
   | T_Lt =>
-    let$ (ctx, (e1, _)) = prems(0) >> Entail(__, HasTy(__, Num));
-    let$ (_, (e2, _)) = prems(1) >> Entail(!ctx, HasTy(__, Num));
-    let$ _ = concl >> Entail(!ctx, HasTy(Lt(!e1, !e2), Bool));
+    let$ (ctx, (e1, _)) = prems(0) >> Entail(__, HasType(__, Num));
+    let$ (_, (e2, _)) = prems(1) >> Entail(!ctx, HasType(__, Num));
+    let$ _ = concl >> Entail(!ctx, HasType(Lt(!e1, !e2), Bool));
     Ok();
   | E_Lt_T =>
     let$ (e1, v1) = prems(0) >> Eval(__, __);
@@ -952,9 +952,9 @@ let verify = (rule: Rule.t, prems: list(t), concl: t): result(unit, failure) =>
     let$ _ = concl >> Entail(!ctx, Syn(Gt(!e1, !e2), Bool));
     Ok();
   | T_Gt =>
-    let$ (ctx, (e1, _)) = prems(0) >> Entail(__, HasTy(__, Num));
-    let$ (_, (e2, _)) = prems(1) >> Entail(!ctx, HasTy(__, Num));
-    let$ _ = concl >> Entail(!ctx, HasTy(Gt(!e1, !e2), Bool));
+    let$ (ctx, (e1, _)) = prems(0) >> Entail(__, HasType(__, Num));
+    let$ (_, (e2, _)) = prems(1) >> Entail(!ctx, HasType(__, Num));
+    let$ _ = concl >> Entail(!ctx, HasType(Gt(!e1, !e2), Bool));
     Ok();
   | E_Gt_T =>
     let$ (e1, v1) = prems(0) >> Eval(__, __);
@@ -972,9 +972,9 @@ let verify = (rule: Rule.t, prems: list(t), concl: t): result(unit, failure) =>
     let$ _ = concl >> Entail(!ctx, Syn(Eq(!e1, !e2), Bool));
     Ok();
   | T_Eq =>
-    let$ (ctx, (e1, _)) = prems(0) >> Entail(__, HasTy(__, Num));
-    let$ (_, (e2, _)) = prems(1) >> Entail(!ctx, HasTy(__, Num));
-    let$ _ = concl >> Entail(!ctx, HasTy(Eq(!e1, !e2), Bool));
+    let$ (ctx, (e1, _)) = prems(0) >> Entail(__, HasType(__, Num));
+    let$ (_, (e2, _)) = prems(1) >> Entail(!ctx, HasType(__, Num));
+    let$ _ = concl >> Entail(!ctx, HasType(Eq(!e1, !e2), Bool));
     Ok();
   | E_Eq_T =>
     let$ (e1, v1) = prems(0) >> Eval(__, __);
@@ -999,11 +999,11 @@ let verify = (rule: Rule.t, prems: list(t), concl: t): result(unit, failure) =>
     let$ _ = concl >> Entail(!ctx, Ana(If(!e_cond, !e_then, !e_else), !t));
     Ok();
   | T_If =>
-    let$ (ctx, (e_cond, _)) = prems(0) >> Entail(__, HasTy(__, Bool));
-    let$ (_, (e_then, t)) = prems(1) >> Entail(!ctx, HasTy(__, __));
-    let$ (_, (e_else, _)) = prems(2) >> Entail(!ctx, HasTy(__, !t));
+    let$ (ctx, (e_cond, _)) = prems(0) >> Entail(__, HasType(__, Bool));
+    let$ (_, (e_then, t)) = prems(1) >> Entail(!ctx, HasType(__, __));
+    let$ (_, (e_else, _)) = prems(2) >> Entail(!ctx, HasType(__, !t));
     let$ _ =
-      concl >> Entail(!ctx, HasTy(If(!e_cond, !e_then, !e_else), !t));
+      concl >> Entail(!ctx, HasType(If(!e_cond, !e_then, !e_else), !t));
     Ok();
   | E_If_T =>
     let$ (e_cond, _) = prems(0) >> Eval(__, True);
@@ -1020,7 +1020,7 @@ let verify = (rule: Rule.t, prems: list(t), concl: t): result(unit, failure) =>
     let$ _ = ctx >> !!MemHasTy(x, t);
     Ok();
   | T_Var =>
-    let$ (ctx, (x, t)) = concl >> Entail(__, HasTy(__, __));
+    let$ (ctx, (x, t)) = concl >> Entail(__, HasType(__, __));
     let$ _ = ctx >> !!MemHasTy(x, t);
     Ok();
   | S_LetAnn =>
@@ -1039,10 +1039,10 @@ let verify = (rule: Rule.t, prems: list(t), concl: t): result(unit, failure) =>
     Ok();
   | T_LetAnn =>
     let$ (ctx, ((x, t_def, e_def, e_body), t)) =
-      concl >> Entail(__, HasTy(LetAnn(__, __, __, __), __));
+      concl >> Entail(__, HasType(LetAnn(__, __, __, __), __));
     let ctx' = ConsHasTy((x, t_def), ctx);
-    let$ _ = prems(0) >> Entail(!ctx, HasTy(!e_def, !t_def));
-    let$ _ = prems(1) >> Entail(!!ctx', HasTy(!e_body, !t));
+    let$ _ = prems(0) >> Entail(!ctx, HasType(!e_def, !t_def));
+    let$ _ = prems(1) >> Entail(!!ctx', HasType(!e_body, !t));
     Ok();
   | S_Let =>
     let$ (ctx, ((x, e_def, e_body), t)) =
@@ -1060,10 +1060,10 @@ let verify = (rule: Rule.t, prems: list(t), concl: t): result(unit, failure) =>
     Ok();
   | T_Let =>
     let$ (ctx, ((x, e_def, e_body), t)) =
-      concl >> Entail(__, HasTy(Let(__, __, __), __));
-    let$ (_, (_, t_def)) = prems(0) >> Entail(!ctx, HasTy(!e_def, __));
+      concl >> Entail(__, HasType(Let(__, __, __), __));
+    let$ (_, (_, t_def)) = prems(0) >> Entail(!ctx, HasType(!e_def, __));
     let ctx' = ConsHasTy((x, t_def), ctx);
-    let$ _ = prems(1) >> Entail(!!ctx', HasTy(!e_body, !t));
+    let$ _ = prems(1) >> Entail(!!ctx', HasType(!e_body, !t));
     Ok();
   | E_Let =>
     let$ ((x, e_def, e_body), v) = concl >> Eval(Let(__, __, __), __);
@@ -1086,10 +1086,10 @@ let verify = (rule: Rule.t, prems: list(t), concl: t): result(unit, failure) =>
     Ok();
   | T_FunAnn =>
     let$ (ctx, ((x, t_in, e_body), (t_in', t_out))) =
-      concl >> Entail(__, HasTy(FunAnn(__, __, __), Arrow(__, __)));
+      concl >> Entail(__, HasType(FunAnn(__, __, __), Arrow(__, __)));
     let$ _ = t_in' >> !t_in;
     let ctx' = ConsHasTy((x, t_in), ctx);
-    let$ _ = prems(0) >> Entail(!!ctx', HasTy(!e_body, !t_out));
+    let$ _ = prems(0) >> Entail(!!ctx', HasType(!e_body, !t_out));
     Ok();
   | A_Fun =>
     let$ (ctx, ((x, e_body), (t_in, t_out))) =
@@ -1099,23 +1099,25 @@ let verify = (rule: Rule.t, prems: list(t), concl: t): result(unit, failure) =>
     Ok();
   | T_Fun =>
     let$ (ctx, ((x, e_body), (t_in, t_out))) =
-      concl >> Entail(__, HasTy(Fun(__, __), Arrow(__, __)));
+      concl >> Entail(__, HasType(Fun(__, __), Arrow(__, __)));
     let ctx' = ConsHasTy((x, t_in), ctx);
-    let$ _ = prems(0) >> Entail(!!ctx', HasTy(!e_body, !t_out));
+    let$ _ = prems(0) >> Entail(!!ctx', HasType(!e_body, !t_out));
     Ok();
   | V_Fun =>
     let$ _ = concl >> Val(Fun(__, __));
     Ok();
   | T_Fix =>
     let$ (ctx, ((x, e), t)) =
-      concl >> Entail(__, HasTy(Fix(__, __), __));
-    let$ _ = prems(0) >> Entail(!!ConsHasTy((x, t), ctx), HasTy(!e, !t));
+      concl >> Entail(__, HasType(Fix(__, __), __));
+    let$ _ =
+      prems(0) >> Entail(!!ConsHasTy((x, t), ctx), HasType(!e, !t));
     Ok();
   | T_FixAnn =>
     let$ (ctx, ((x, t, e), t')) =
-      concl >> Entail(__, HasTy(FixAnn(__, __, __), __));
+      concl >> Entail(__, HasType(FixAnn(__, __, __), __));
     let$ _ = t >> !t';
-    let$ _ = prems(0) >> Entail(!!ConsHasTy((x, t), ctx), HasTy(!e, !t));
+    let$ _ =
+      prems(0) >> Entail(!!ConsHasTy((x, t), ctx), HasType(!e, !t));
     Ok();
   | E_Fix =>
     let$ (e, v) = concl >> Eval(__, __);
@@ -1131,10 +1133,10 @@ let verify = (rule: Rule.t, prems: list(t), concl: t): result(unit, failure) =>
     Ok();
   | T_Ap =>
     let$ (ctx, ((e_fun, e_arg), t_out)) =
-      concl >> Entail(__, HasTy(Ap(__, __), __));
+      concl >> Entail(__, HasType(Ap(__, __), __));
     let$ (_, (_, (t_in, _))) =
-      prems(0) >> Entail(!ctx, HasTy(!e_fun, Arrow(__, !t_out)));
-    let$ _ = prems(1) >> Entail(!ctx, HasTy(!e_arg, !t_in));
+      prems(0) >> Entail(!ctx, HasType(!e_fun, Arrow(__, !t_out)));
+    let$ _ = prems(1) >> Entail(!ctx, HasType(!e_arg, !t_in));
     Ok();
   | E_Ap =>
     let$ ((e_fun, e_arg), v) = concl >> Eval(Ap(__, __), __);
@@ -1153,9 +1155,10 @@ let verify = (rule: Rule.t, prems: list(t), concl: t): result(unit, failure) =>
     let$ _ = concl >> Entail(!ctx, Ana(Pair(!el, !er), Prod(!tl, !tr)));
     Ok();
   | T_Pair =>
-    let$ (ctx, (el, tl)) = prems(0) >> Entail(__, HasTy(__, __));
-    let$ (_, (er, tr)) = prems(1) >> Entail(!ctx, HasTy(__, __));
-    let$ _ = concl >> Entail(!ctx, HasTy(Pair(!el, !er), Prod(!tl, !tr)));
+    let$ (ctx, (el, tl)) = prems(0) >> Entail(__, HasType(__, __));
+    let$ (_, (er, tr)) = prems(1) >> Entail(!ctx, HasType(__, __));
+    let$ _ =
+      concl >> Entail(!ctx, HasType(Pair(!el, !er), Prod(!tl, !tr)));
     Ok();
   | E_Pair =>
     let$ (el, vl) = prems(0) >> Eval(__, __);
@@ -1185,11 +1188,11 @@ let verify = (rule: Rule.t, prems: list(t), concl: t): result(unit, failure) =>
     Ok();
   | T_LetPair =>
     let$ (ctx, ((x, y, e_def, e_body), t)) =
-      concl >> Entail(__, HasTy(LetPair(__, __, __, __), __));
+      concl >> Entail(__, HasType(LetPair(__, __, __, __), __));
     let$ (_, (_, (tl, tr))) =
-      prems(0) >> Entail(!ctx, HasTy(!e_def, Prod(__, __)));
+      prems(0) >> Entail(!ctx, HasType(!e_def, Prod(__, __)));
     let ctx_xy = ConsHasTy2((x, tl), (y, tr), ctx);
-    let$ _ = prems(1) >> Entail(!!ctx_xy, HasTy(!e_body, !t));
+    let$ _ = prems(1) >> Entail(!!ctx_xy, HasType(!e_body, !t));
     Ok();
   | E_LetPair =>
     let$ ((x, y, e_def, e_body), v) =
@@ -1203,8 +1206,8 @@ let verify = (rule: Rule.t, prems: list(t), concl: t): result(unit, failure) =>
     let$ _ = prems(0) >> Entail(!ctx, Syn(!e, Prod(!tl, __)));
     Ok();
   | T_PrjL =>
-    let$ (ctx, (e, tl)) = concl >> Entail(__, HasTy(PrjL(__), __));
-    let$ _ = prems(0) >> Entail(!ctx, HasTy(!e, Prod(!tl, __)));
+    let$ (ctx, (e, tl)) = concl >> Entail(__, HasType(PrjL(__), __));
+    let$ _ = prems(0) >> Entail(!ctx, HasType(!e, Prod(!tl, __)));
     Ok();
   | E_PrjL =>
     let$ (e, vl) = concl >> Eval(PrjL(__), __);
@@ -1215,8 +1218,8 @@ let verify = (rule: Rule.t, prems: list(t), concl: t): result(unit, failure) =>
     let$ _ = prems(0) >> Entail(!ctx, Syn(!e, Prod(__, !tr)));
     Ok();
   | T_PrjR =>
-    let$ (ctx, (e, tr)) = concl >> Entail(__, HasTy(PrjR(__), __));
-    let$ _ = prems(0) >> Entail(!ctx, HasTy(!e, Prod(__, !tr)));
+    let$ (ctx, (e, tr)) = concl >> Entail(__, HasType(PrjR(__), __));
+    let$ _ = prems(0) >> Entail(!ctx, HasType(!e, Prod(__, !tr)));
     Ok();
   | E_PrjR =>
     let$ (e, vr) = concl >> Eval(PrjR(__), __);
@@ -1227,8 +1230,8 @@ let verify = (rule: Rule.t, prems: list(t), concl: t): result(unit, failure) =>
     let$ _ = concl >> Entail(!ctx, Ana(InjL(!e), Sum(!tl, __)));
     Ok();
   | T_InjL =>
-    let$ (ctx, (e, tl)) = prems(0) >> Entail(__, HasTy(__, __));
-    let$ _ = concl >> Entail(!ctx, HasTy(InjL(!e), Sum(!tl, __)));
+    let$ (ctx, (e, tl)) = prems(0) >> Entail(__, HasType(__, __));
+    let$ _ = concl >> Entail(!ctx, HasType(InjL(!e), Sum(!tl, __)));
     Ok();
   | E_InjL =>
     let$ (e, v) = prems(0) >> Eval(__, __);
@@ -1243,8 +1246,8 @@ let verify = (rule: Rule.t, prems: list(t), concl: t): result(unit, failure) =>
     let$ _ = concl >> Entail(!ctx, Ana(InjR(!e), Sum(__, !tr)));
     Ok();
   | T_InjR =>
-    let$ (ctx, (e, tr)) = prems(0) >> Entail(__, HasTy(__, __));
-    let$ _ = concl >> Entail(!ctx, HasTy(InjR(!e), Sum(__, !tr)));
+    let$ (ctx, (e, tr)) = prems(0) >> Entail(__, HasType(__, __));
+    let$ _ = concl >> Entail(!ctx, HasType(InjR(!e), Sum(__, !tr)));
     Ok();
   | E_InjR =>
     let$ (e, v) = prems(0) >> Eval(__, __);
@@ -1272,13 +1275,13 @@ let verify = (rule: Rule.t, prems: list(t), concl: t): result(unit, failure) =>
     Ok();
   | T_Case =>
     let$ (ctx, ((e_scrut, x, el, y, er), t)) =
-      concl >> Entail(__, HasTy(Case(__, __, __, __, __), __));
+      concl >> Entail(__, HasType(Case(__, __, __, __, __), __));
     let$ (_, (_, (tl, tr))) =
-      prems(0) >> Entail(!ctx, HasTy(!e_scrut, Sum(__, __)));
+      prems(0) >> Entail(!ctx, HasType(!e_scrut, Sum(__, __)));
     let$ _ =
-      prems(1) >> Entail(!!ConsHasTy((x, tl), ctx), HasTy(!el, !t));
+      prems(1) >> Entail(!!ConsHasTy((x, tl), ctx), HasType(!el, !t));
     let$ _ =
-      prems(2) >> Entail(!!ConsHasTy((y, tr), ctx), HasTy(!er, !t));
+      prems(2) >> Entail(!!ConsHasTy((y, tr), ctx), HasType(!er, !t));
     Ok();
   | E_Case_L =>
     let$ ((e_scrut, x, el, _y, _er), v) =
@@ -1293,10 +1296,11 @@ let verify = (rule: Rule.t, prems: list(t), concl: t): result(unit, failure) =>
     let$ _ = prems(1) >> Eval(!!Subst((v_data, y), er), !v);
     Ok();
   | T_Roll =>
-    let$ (ctx, (e_body, t)) = concl >> Entail(__, HasTy(Roll(__), __));
+    let$ (ctx, (e_body, t)) = concl >> Entail(__, HasType(Roll(__), __));
     let$ (a, t_body) = t >> Rec(__, __);
     let$ _ =
-      prems(0) >> Entail(!ctx, HasTy(!e_body, !!SubstTy((t, a), t_body)));
+      prems(0)
+      >> Entail(!ctx, HasType(!e_body, !!SubstTy((t, a), t_body)));
     Ok();
   | E_Roll =>
     let$ (e, v) = concl >> Eval(Roll(__), Roll(__));
@@ -1307,10 +1311,11 @@ let verify = (rule: Rule.t, prems: list(t), concl: t): result(unit, failure) =>
     let$ _ = concl >> Val(Roll(!e));
     Ok();
   | T_Unroll =>
-    let$ (ctx, (e, t)) = prems(0) >> Entail(__, HasTy(__, __));
+    let$ (ctx, (e, t)) = prems(0) >> Entail(__, HasType(__, __));
     let$ (a, t_body) = t >> Rec(__, __);
     let$ _ =
-      concl >> Entail(!ctx, HasTy(Unroll(!e), !!SubstTy((t, a), t_body)));
+      concl
+      >> Entail(!ctx, HasType(Unroll(!e), !!SubstTy((t, a), t_body)));
     Ok();
   | E_Unroll =>
     let$ (e, v) = prems(0) >> Eval(__, Roll(__));
diff --git a/src/haz3lcore/dynamics/Transition.re b/src/haz3lcore/dynamics/Transition.re
index 31e182ccce..08aaa1aa59 100644
--- a/src/haz3lcore/dynamics/Transition.re
+++ b/src/haz3lcore/dynamics/Transition.re
@@ -253,7 +253,16 @@ module Transition = (EV: EV_MODE) => {
         | Hole(s) => Hole(s)
         | Val(e) => Val(go_exp(e))
         | Eval(e1, e2) => Eval(go_exp(e1), go_exp(e2))
-        | Entail(p1, p2) => Entail(go_prop(p1), go_prop(p2))
+        | Entail(ctx, p) => Entail(go_ctxt(ctx), go_prop(p))
+        };
+      term |> rewrap;
+    }
+    and go_ctxt = ctxt => {
+      let (term, rewrap) = Drv.Ctxt.unwrap(ctxt);
+      let term: Drv.Ctxt.term =
+        switch (term) {
+        | Hole(s) => Hole(s)
+        | Ctxt(p) => Ctxt(go_prop(p))
         };
       term |> rewrap;
     }
@@ -262,7 +271,7 @@ module Transition = (EV: EV_MODE) => {
       let term: Drv.Prop.term =
         switch (term) {
         | Hole(s) => Hole(s)
-        | HasTy(e, t) => HasTy(go_exp(e), t)
+        | HasType(e, t) => HasType(go_exp(e), t)
         | Syn(e, t) => Syn(go_exp(e), t)
         | Ana(e, t) => Ana(go_exp(e), t)
         | Var(x) => Var(x)
diff --git a/src/haz3lcore/lang/Form.re b/src/haz3lcore/lang/Form.re
index 05efd24282..8622257523 100644
--- a/src/haz3lcore/lang/Form.re
+++ b/src/haz3lcore/lang/Form.re
@@ -109,7 +109,7 @@ let keywords = [
   "val",
   "eval",
   "entail",
-  "typ",
+  "hastype",
   "syn",
   "ana",
 ];
@@ -248,7 +248,13 @@ let atomic_forms: list((string, (string => bool, list(Mold.t)))) = [
   ("float_lit", (is_float, [mk_op(Exp, []), mk_op(Pat, [])])),
   ("bool_lit", (is_bool, [mk_op(Exp, []), mk_op(Pat, [])])),
   ("undefined_lit", (is_undefined, [mk_op(Exp, []), mk_op(Pat, [])])),
-  ("empty_list", (is_empty_list, [mk_op(Exp, []), mk_op(Pat, [])])),
+  (
+    "empty_list",
+    (
+      is_empty_list,
+      [mk_op(Exp, []), mk_op(Pat, []), mk_op(Drv(Ctxt), [])],
+    ),
+  ),
   (
     "empty_tuple",
     (
@@ -258,7 +264,6 @@ let atomic_forms: list((string, (string => bool, list(Mold.t)))) = [
         mk_op(Pat, []),
         mk_op(Typ, []),
         mk_op(Drv(Exp), []),
-        mk_op(Drv(Prop), []),
       ],
     ),
   ),
@@ -373,23 +378,27 @@ 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)]))),
   (
-    "prop_alias",
-    mk(ds, ["prop", "=", "in"], mk_pre(P.let_, Exp, [Pat, Drv(Prop)])),
+    "of_alfa_exp",
+    mk(ds, ["of_alfa_exp", "end"], mk_op(Exp, [Drv(Exp)])),
   ),
-  (
-    "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)]))),
+  // ("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_ctxt", mk(ds, ["of_ctxt", "end"], mk_op(Exp, [Drv(Ctxt)]))),
+  // ("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", "end"], mk_op(Exp, [Exp]))),
+  ("val", mk(ds, ["val", "end"], mk_op(Drv(Jdmt), [Drv(Exp)]))),
+  ("fake_eval", mk(ds, ["eval", "to", "end"], mk_op(Exp, [Exp, Exp]))),
   (
     "eval",
     mk(
@@ -398,20 +407,63 @@ let forms: list((string, t)) = [
       mk_op(Drv(Jdmt), [Drv(Exp), Drv(Exp)]),
     ),
   ),
+  // Note(zhiyao): there is no "fake_entail" because it will diable entail_hastype, entail_syn, and entail_ana
   (
     "entail",
     mk(
-      ii,
+      ds,
       ["entail", "|-", "end"],
-      mk_op(Drv(Jdmt), [Drv(Prop), Drv(Prop)]),
+      mk_op(Drv(Jdmt), [Drv(Ctxt), Drv(Prop)]),
+    ),
+  ),
+  (
+    "fake_entail_hastype",
+    mk(
+      ds,
+      ["entail_hastype", "|-", ":", "end"],
+      mk_op(Exp, [Exp, Exp, Exp]),
+    ),
+  ),
+  (
+    "entail_hastype",
+    mk(
+      ii,
+      ["entail_hastype", "|-", ":", "end"],
+      mk_op(Drv(Jdmt), [Drv(Ctxt), Drv(Exp), Drv(Typ)]),
+    ),
+  ),
+  (
+    "fake_entail_syn",
+    mk(ds, ["entail_syn", "|-", "=>", "end"], mk_op(Exp, [Exp, Exp, Exp])),
+  ),
+  (
+    "entail_syn",
+    mk(
+      ii,
+      ["entail_syn", "|-", "=>", "end"],
+      mk_op(Drv(Jdmt), [Drv(Ctxt), Drv(Exp), Drv(Typ)]),
+    ),
+  ),
+  (
+    "fake_entail_ana",
+    mk(ds, ["entail_ana", "|-", "<=", "end"], mk_op(Exp, [Exp, Exp, Exp])),
+  ),
+  (
+    "entail_ana",
+    mk(
+      ii,
+      ["entail_ana", "|-", "<=", "end"],
+      mk_op(Drv(Jdmt), [Drv(Ctxt), Drv(Exp), Drv(Typ)]),
     ),
   ),
+  // Drv(Ctxt)
+  ("list_lit_ctxt", mk(ii, ["[", "]"], mk_op(Drv(Ctxt), [Drv(Prop)]))),
   // Drv(Prop)
   (
-    "hasty",
+    "hastype",
     mk(
       ds,
-      ["typ", ":"],
+      ["hastype", ":"],
       mk_pre'(P.fun_, Drv(Prop), Drv(Prop), [Drv(Exp)], Drv(Typ)),
     ),
   ),
diff --git a/src/haz3lcore/lang/Sort.re b/src/haz3lcore/lang/Sort.re
index 46469fc098..3aedde2c90 100644
--- a/src/haz3lcore/lang/Sort.re
+++ b/src/haz3lcore/lang/Sort.re
@@ -2,6 +2,7 @@ module DrvSort = {
   [@deriving (show({with_path: false}), sexp, yojson)]
   type t =
     | Jdmt
+    | Ctxt
     | Prop
     | Exp
     | Pat
@@ -12,6 +13,7 @@ module DrvSort = {
     fun
     | Jdmt => "Jdmt"
     | Prop => "Prop"
+    | Ctxt => "Ctxt"
     | Exp => "ALFA_Exp"
     | Pat => "ALFA_Pat"
     | Typ => "ALFA_Typ"
@@ -20,6 +22,7 @@ module DrvSort = {
   let class_of =
     fun
     | Jdmt => "Drv"
+    | Ctxt => "Drv"
     | Prop => "Drv"
     | Exp => "Exp"
     | Pat => "Pat"
@@ -31,6 +34,7 @@ module DrvSort = {
   let to_string =
     fun
     | Jdmt => "Jdmt"
+    | Ctxt => "Ctxt"
     | Prop => "Prop"
     | Exp => "ALFA_Exp"
     | Pat => "ALFA_Pat"
@@ -40,6 +44,7 @@ module DrvSort = {
   let to_string_verbose =
     fun
     | Jdmt => "judgement"
+    | Ctxt => "context"
     | Prop => "proposition"
     | Exp => "ALFA expression"
     | Pat => "ALFA pattern"
diff --git a/src/haz3lcore/lang/term/Drv.re b/src/haz3lcore/lang/term/Drv.re
index f37a39c8dc..9ba5c1f24e 100644
--- a/src/haz3lcore/lang/term/Drv.re
+++ b/src/haz3lcore/lang/term/Drv.re
@@ -1,5 +1,6 @@
 include Term.Drv;
 module Jdmt = Term.Jdmt;
+module Ctxt = Term.Ctxt;
 module Prop = Term.Prop;
 module Exp = Term.ALFA_Exp;
 module Pat = Term.ALFA_Pat;
diff --git a/src/haz3lcore/statics/MakeTerm.re b/src/haz3lcore/statics/MakeTerm.re
index 837b505115..111b071ee2 100644
--- a/src/haz3lcore/statics/MakeTerm.re
+++ b/src/haz3lcore/statics/MakeTerm.re
@@ -146,6 +146,7 @@ let rec go_s = (s: Sort.t, skel: Skel.t, seg: Segment.t): Term.Any.t =>
     Drv(
       switch (drv) {
       | Jdmt => Jdmt(jdmt(unsorted(skel, seg)))
+      | Ctxt => Ctxt(ctxt(unsorted(skel, seg)))
       | Prop => Prop(prop(unsorted(skel, seg)))
       | Exp => Exp(alfa_exp(unsorted(skel, seg)))
       | Pat => Pat(alfa_pat(unsorted(skel, seg)))
@@ -186,17 +187,30 @@ and jdmt_term: unsorted => (Drv.Jdmt.term, list(Id.t)) = {
   let ret = (tm: Drv.Jdmt.term) => (tm, []);
   let hole = unsorted => Drv.Jdmt.hole(kids_of_unsorted(unsorted));
   fun
-  | Op(([(_id, (["val", "end"], [Drv(Exp(e))]))], [])) => ret(Val(e))
-  | Op((
-      [(_id, (["eval", "to", "end"], [Drv(Exp(l)), Drv(Exp(r))]))],
-      [],
-    )) =>
-    ret(Eval(l, r))
-  | Op((
-      [(_id, (["entail", "|-", "end"], [Drv(Prop(l)), Drv(Prop(r))]))],
-      [],
-    )) =>
-    ret(Entail(l, r))
+  | Op(([(_id, t)], [])) as tm =>
+    switch (t) {
+    | (["val", "end"], [Drv(Exp(e))]) => ret(Val(e))
+    | (["eval", "to", "end"], [Drv(Exp(l)), Drv(Exp(r))]) =>
+      ret(Eval(l, r))
+    | (["entail", "|-", "end"], [Drv(Ctxt(l)), Drv(Prop(r))]) =>
+      ret(Entail(l, r))
+    | (
+        ["entail_hastype", "|-", ":", "end"],
+        [Drv(Ctxt(l)), Drv(Exp(e)), Drv(Typ(t))],
+      ) =>
+      ret(Entail(l, HasType(e, t) |> Drv.Prop.fresh))
+    | (
+        ["entail_syn", "|-", "=>", "end"],
+        [Drv(Ctxt(l)), Drv(Exp(e)), Drv(Typ(t))],
+      ) =>
+      ret(Entail(l, Syn(e, t) |> Drv.Prop.fresh))
+    | (
+        ["entail_ana", "|-", "<=", "end"],
+        [Drv(Ctxt(l)), Drv(Exp(e)), Drv(Typ(t))],
+      ) =>
+      ret(Entail(l, Ana(e, t) |> Drv.Prop.fresh))
+    | _ => ret(hole(tm))
+    }
   // | Post(Drv(Exp(l)), ([(_id, ([".val"], []))], [])) => ret(Val(l))
   // | Bin(Drv(Exp(l)), ([(_id, (["$>"], []))], []), Drv(Exp(r))) =>
   //   ret(Eval(l, r))
@@ -205,6 +219,26 @@ and jdmt_term: unsorted => (Drv.Jdmt.term, list(Id.t)) = {
   | _ as tm => ret(hole(tm));
 }
 
+and ctxt = unsorted => {
+  let (term, inner_ids) = ctxt_term(unsorted);
+  let ids = ids(unsorted) @ inner_ids;
+  return(p => Drv(Ctxt(p)), ids, {ids, copied: false, term});
+}
+
+and ctxt_term: unsorted => (Drv.Ctxt.term, list(Id.t)) = {
+  let ret = (tm: Drv.Ctxt.term) => (tm, []);
+  let hole = unsorted => Drv.Ctxt.hole(kids_of_unsorted(unsorted));
+  fun
+  | Op(([(_id, t)], [])) as tm =>
+    switch (t) {
+    | ([t], []) when Form.is_empty_list(t) =>
+      ret(Ctxt(Drv.Prop.fresh(Tuple([]))))
+    | (["[", "]"], [Drv(Prop(body))]) => ret(Ctxt(body))
+    | _ => ret(hole(tm))
+    }
+  | _ as tm => ret(hole(tm));
+}
+
 and prop = unsorted => {
   let (term, inner_ids) = prop_term(unsorted);
   let ids = ids(unsorted) @ inner_ids;
@@ -216,7 +250,6 @@ and prop_term: unsorted => (Drv.Prop.term, list(Id.t)) = {
   fun
   | Op(([(_id, ([t], []))], [])) as tm =>
     switch (t) {
-    | "()" => ret(Tuple([]))
     | "Truth" => ret(Truth)
     | "Falsity" => ret(Falsity)
     | _ when Form.is_typ_var(t) => ret(Var(t))
@@ -227,7 +260,7 @@ and prop_term: unsorted => (Drv.Prop.term, list(Id.t)) = {
   | Op(([(_id, (["{", "}"], [Pat(var)]))], [])) => ret(Abbr(var))
   | Pre(([(_id, ([t1, t2], [Drv(Exp(l))]))], []), Drv(Typ(r))) as tm =>
     switch (t1, t2) {
-    | ("typ", ":") => ret(HasTy(l, r))
+    | ("hastype", ":") => ret(HasType(l, r))
     | ("syn", "=>") => ret(Syn(l, r))
     | ("ana", "<=") => ret(Ana(l, r))
     | _ => ret(hole(tm))
@@ -427,13 +460,16 @@ and exp_term: unsorted => (UExp.term, list(Id.t)) = {
           Match(scrut, rules),
           ids,
         )
-      | (["of_Typ", "end"], [Drv(Typ(ty))]) => ret(Term(Drv(Typ(ty))))
-      | (["of_Exp", "end"], [Drv(Exp(e))]) => ret(Term(Drv(Exp(e))))
-      | (["of_Pat", "end"], [Drv(Pat(p))]) => ret(Term(Drv(Pat(p))))
-      | (["of_TPat", "end"], [Drv(TPat(tp))]) =>
-        ret(Term(Drv(TPat(tp))))
-      | (["of_Prop", "end"], [Drv(Prop(p))]) => ret(Term(Drv(Prop(p))))
-      | (["of_Jdmt", "end"], [Drv(Jdmt(j))]) => ret(Term(Drv(Jdmt(j))))
+      // | (["of_typ", "end"], [Drv(Typ(ty))]) => ret(Term(Drv(Typ(ty))))
+      | (["of_alfa_exp", "end"], [Drv(Exp(e))]) =>
+        ret(Term(Drv(Exp(e))))
+      // | (["of_pat", "end"], [Drv(Pat(p))]) => ret(Term(Drv(Pat(p))))
+      // | (["of_tpat", "end"], [Drv(TPat(tp))]) =>
+      //   ret(Term(Drv(TPat(tp))))
+      | (["of_ctxt", "end"], [Drv(Ctxt(ctx))]) =>
+        ret(Term(Drv(Ctxt(ctx))))
+      | (["of_prop", "end"], [Drv(Prop(p))]) => ret(Term(Drv(Prop(p))))
+      // | (["of_jdmt", "end"], [Drv(Jdmt(j))]) => ret(Term(Drv(Jdmt(j))))
       | ([t], []) when t != " " && !Form.is_explicit_hole(t) =>
         ret(Invalid(t))
       | _ => ret(hole(tm))
diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re
index f3fd9a5534..7da1b5701f 100644
--- a/src/haz3lcore/statics/Statics.re
+++ b/src/haz3lcore/statics/Statics.re
@@ -183,22 +183,26 @@ and drv_to_info_map =
       | 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, ~can_tuple=true)
-        |> snd
-        |> go_prop(p2, ~can_tuple=false)
-        |> snd
+      | Entail(ctx, p) =>
+        m |> go_ctxt(ctx) |> snd |> go_prop(p, ~can_tuple=false) |> snd
       };
     add(Jdmt(jdmt), info, m);
   }
+  and go_ctxt = (ctxt: Drv.Ctxt.t, m) => {
+    let info = DrvInfo.derived_ctxt(ctxt, ~ancestors);
+    let add' = add(Ctxt(ctxt), Ctxt(info));
+    switch (ctxt.term) {
+    | Hole(_) => m |> add'
+    | Ctxt(p) => m |> go_prop(p, ~can_tuple=true) |> snd |> add'
+    };
+  }
   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)
+    | HasType(e, t)
     | Syn(e, t)
     | Ana(e, t) => m |> go_exp'(e) |> snd |> go_typ(t) |> snd |> add'
     | Var(_) => m |> add'
@@ -356,6 +360,7 @@ and drv_to_info_map =
   };
   switch (drv) {
   | Jdmt(jdmt) => go_jdmt(jdmt, m)
+  | Ctxt(ctxt) => go_ctxt(ctxt, 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)
diff --git a/src/haz3lcore/statics/Term.re b/src/haz3lcore/statics/Term.re
index 0d19bc4835..c06fd683af 100644
--- a/src/haz3lcore/statics/Term.re
+++ b/src/haz3lcore/statics/Term.re
@@ -625,6 +625,7 @@ module Any = {
   let rec ids =
     fun
     | Drv(Jdmt(tm)) => tm.ids
+    | Drv(Ctxt(tm)) => tm.ids
     | Drv(Prop(tm)) => tm.ids
     | Drv(Exp(tm)) => tm.ids
     | Drv(Pat(tm)) => tm.ids
@@ -652,6 +653,7 @@ module Any = {
   let rep_id =
     fun
     | Drv(Jdmt(tm)) => Jdmt.rep_id(tm)
+    | Drv(Ctxt(tm)) => Ctxt.rep_id(tm)
     | Drv(Prop(tm)) => Prop.rep_id(tm)
     | Drv(Exp(tm)) => ALFA_Exp.rep_id(tm)
     | Drv(Pat(tm)) => ALFA_Pat.rep_id(tm)
diff --git a/src/haz3lcore/statics/TermBase.re b/src/haz3lcore/statics/TermBase.re
index 69fd37f3d8..05df8988fb 100644
--- a/src/haz3lcore/statics/TermBase.re
+++ b/src/haz3lcore/statics/TermBase.re
@@ -1247,6 +1247,7 @@ and Drv: {
   [@deriving (show({with_path: false}), sexp, yojson)]
   type t =
     | Jdmt(Jdmt.t)
+    | Ctxt(Ctxt.t)
     | Prop(Prop.t)
     | Exp(ALFA_Exp.t)
     | Pat(ALFA_Pat.t)
@@ -1255,6 +1256,7 @@ and Drv: {
 
   type mapper = {
     f_jdmt: (Jdmt.t => Jdmt.t, Jdmt.t) => Jdmt.t,
+    f_ctxt: (Ctxt.t => Ctxt.t, Ctxt.t) => Ctxt.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,
@@ -1271,6 +1273,7 @@ and Drv: {
   [@deriving (show({with_path: false}), sexp, yojson)]
   type t =
     | Jdmt(Jdmt.t)
+    | Ctxt(Ctxt.t)
     | Prop(Prop.t)
     | Exp(ALFA_Exp.t)
     | Pat(ALFA_Pat.t)
@@ -1279,6 +1282,7 @@ and Drv: {
 
   type mapper = {
     f_jdmt: (Jdmt.t => Jdmt.t, Jdmt.t) => Jdmt.t,
+    f_ctxt: (Ctxt.t => Ctxt.t, Ctxt.t) => Ctxt.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,
@@ -1288,6 +1292,7 @@ and Drv: {
 
   let drv_continue = {
     f_jdmt: continue,
+    f_ctxt: continue,
     f_prop: continue,
     f_exp: continue,
     f_pat: continue,
@@ -1296,13 +1301,14 @@ and Drv: {
   };
 
   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;
+    let {f_jdmt, f_ctxt, 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_ctxt,
           ~f_prop,
           ~f_exp,
           ~f_pat,
@@ -1311,6 +1317,19 @@ and Drv: {
           jdmt,
         ),
       )
+    | Ctxt(ctxt) =>
+      Ctxt(
+        Ctxt.map_term(
+          ~f_hazel_pat,
+          ~f_ctxt,
+          ~f_prop,
+          ~f_exp,
+          ~f_pat,
+          ~f_typ,
+          ~f_tpat,
+          ctxt,
+        ),
+      )
     | Prop(prop) =>
       Prop(
         Prop.map_term(
@@ -1337,6 +1356,8 @@ and Drv: {
     switch (x, y) {
     | (Jdmt(j1), Jdmt(j2)) => Jdmt.fast_equal(j1, j2)
     | (Jdmt(_), _) => false
+    | (Ctxt(c1), Ctxt(c2)) => Ctxt.fast_equal(c1, c2)
+    | (Ctxt(_), _) => false
     | (Prop(p1), Prop(p2)) => Prop.fast_equal(p1, p2)
     | (Prop(_), _) => false
     | (Exp(e1), Exp(e2)) => ALFA_Exp.fast_equal(e1, e2)
@@ -1355,13 +1376,14 @@ and Jdmt: {
     | Hole(TypeHole.t)
     | Val(ALFA_Exp.t)
     | Eval(ALFA_Exp.t, ALFA_Exp.t)
-    | Entail(Prop.t, Prop.t)
+    | Entail(Ctxt.t, Prop.t)
   and t = IdTagged.t(term);
 
   let map_term:
     (
       ~f_hazel_pat: Pat.t => Pat.t=?,
       ~f_jdmt: (Jdmt.t => Jdmt.t, Jdmt.t) => Jdmt.t=?,
+      ~f_ctxt: (Ctxt.t => Ctxt.t, Ctxt.t) => Ctxt.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=?,
@@ -1378,13 +1400,14 @@ and Jdmt: {
     | Hole(TypeHole.t)
     | Val(ALFA_Exp.t)
     | Eval(ALFA_Exp.t, ALFA_Exp.t)
-    | Entail(Prop.t, Prop.t)
+    | Entail(Ctxt.t, Prop.t)
   and t = IdTagged.t(term);
 
   let map_term =
       (
         ~f_hazel_pat=continue,
         ~f_jdmt=continue,
+        ~f_ctxt=continue,
         ~f_prop=continue,
         ~f_exp=continue,
         ~f_pat=continue,
@@ -1392,6 +1415,16 @@ and Jdmt: {
         ~f_tpat=continue,
         x,
       ) => {
+    let ctxt_map_term =
+      Ctxt.map_term(
+        ~f_hazel_pat,
+        ~f_ctxt,
+        ~f_prop,
+        ~f_exp,
+        ~f_pat,
+        ~f_typ,
+        ~f_tpat,
+      );
     let prop_map_term =
       Prop.map_term(~f_hazel_pat, ~f_prop, ~f_exp, ~f_pat, ~f_typ, ~f_tpat);
     let exp_map_term =
@@ -1401,9 +1434,9 @@ and Jdmt: {
       term:
         switch (term) {
         | Hole(_) => term
-        | Val(p) => Val(exp_map_term(p))
-        | Eval(p1, p2) => Eval(exp_map_term(p1), exp_map_term(p2))
-        | Entail(p1, p2) => Entail(prop_map_term(p1), prop_map_term(p2))
+        | Val(e) => Val(exp_map_term(e))
+        | Eval(e1, e2) => Eval(exp_map_term(e1), exp_map_term(e2))
+        | Entail(ctx, p) => Entail(ctxt_map_term(ctx), prop_map_term(p))
         },
     };
     x |> f_jdmt(rec_call);
@@ -1418,15 +1451,74 @@ and Jdmt: {
       ALFA_Exp.fast_equal(p1, p1') && ALFA_Exp.fast_equal(p2, p2')
     | (Eval(_, _), _) => false
     | (Entail(p1, p2), Entail(p1', p2')) =>
-      Prop.fast_equal(p1, p1') && Prop.fast_equal(p2, p2')
+      Ctxt.fast_equal(p1, p1') && Prop.fast_equal(p2, p2')
     | (Entail(_, _), _) => false
     };
 }
+and Ctxt: {
+  [@deriving (show({with_path: false}), sexp, yojson)]
+  type term =
+    | Hole(TypeHole.t)
+    | Ctxt(Prop.t)
+  and t = IdTagged.t(term);
+
+  let map_term:
+    (
+      ~f_hazel_pat: Pat.t => Pat.t=?,
+      ~f_ctxt: (Ctxt.t => Ctxt.t, Ctxt.t) => Ctxt.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=?,
+      ~f_typ: (ALFA_Typ.t => ALFA_Typ.t, ALFA_Typ.t) => ALFA_Typ.t=?,
+      ~f_tpat: (ALFA_TPat.t => ALFA_TPat.t, ALFA_TPat.t) => ALFA_TPat.t=?,
+      t
+    ) =>
+    t;
+
+  let fast_equal: (t, t) => bool;
+} = {
+  [@deriving (show({with_path: false}), sexp, yojson)]
+  type term =
+    | Hole(TypeHole.t)
+    | Ctxt(Prop.t)
+  and t = IdTagged.t(term);
+
+  let map_term =
+      (
+        ~f_hazel_pat=continue,
+        ~f_ctxt=continue,
+        ~f_prop=continue,
+        ~f_exp=continue,
+        ~f_pat=continue,
+        ~f_typ=continue,
+        ~f_tpat=continue,
+        x,
+      ) => {
+    let prop_map_term =
+      Prop.map_term(~f_hazel_pat, ~f_prop, ~f_exp, ~f_pat, ~f_typ, ~f_tpat);
+    let rec_call = ({term, _} as exp: t) => {
+      ...exp,
+      term:
+        switch (term) {
+        | Hole(_) => term
+        | Ctxt(x) => Ctxt(prop_map_term(x))
+        },
+    };
+    x |> f_ctxt(rec_call);
+  };
+
+  let fast_equal = (x, y) => {
+    switch (x |> IdTagged.term_of, y |> IdTagged.term_of) {
+    | (Ctxt(x), Ctxt(y)) => Prop.fast_equal(x, y)
+    | _ => false
+    };
+  };
+}
 and Prop: {
   [@deriving (show({with_path: false}), sexp, yojson)]
   type term =
     | Hole(TypeHole.t)
-    | HasTy(ALFA_Exp.t, ALFA_Typ.t)
+    | HasType(ALFA_Exp.t, ALFA_Typ.t)
     | Syn(ALFA_Exp.t, ALFA_Typ.t)
     | Ana(ALFA_Exp.t, ALFA_Typ.t)
     | Var(Var.t)
@@ -1457,7 +1549,7 @@ and Prop: {
   [@deriving (show({with_path: false}), sexp, yojson)]
   type term =
     | Hole(TypeHole.t)
-    | HasTy(ALFA_Exp.t, ALFA_Typ.t)
+    | HasType(ALFA_Exp.t, ALFA_Typ.t)
     | Syn(ALFA_Exp.t, ALFA_Typ.t)
     | Ana(ALFA_Exp.t, ALFA_Typ.t)
     | Var(Var.t)
@@ -1491,7 +1583,7 @@ and Prop: {
       term:
         switch (term) {
         | Hole(_) => term
-        | HasTy(e, t) => HasTy(exp_map_term(e), typ_map_term(t))
+        | HasType(e, t) => HasType(exp_map_term(e), typ_map_term(t))
         | Syn(e, t) => Syn(exp_map_term(e), typ_map_term(t))
         | Ana(e, t) => Ana(exp_map_term(e), typ_map_term(t))
         | Var(v) => Var(v)
@@ -1511,9 +1603,9 @@ and Prop: {
   let fast_equal = (x, y) =>
     switch (x |> IdTagged.term_of, y |> IdTagged.term_of) {
     | (Hole(_), _) => false
-    | (HasTy(e1, t1), HasTy(e2, t2)) =>
+    | (HasType(e1, t1), HasType(e2, t2)) =>
       ALFA_Exp.fast_equal(e1, e2) && ALFA_Typ.fast_equal(t1, t2)
-    | (HasTy(_), _) => false
+    | (HasType(_), _) => false
     | (Syn(e1, t1), Syn(e2, t2)) =>
       ALFA_Exp.fast_equal(e1, e2) && ALFA_Typ.fast_equal(t1, t2)
     | (Syn(_), _) => false
diff --git a/src/haz3lcore/tiles/Segment.re b/src/haz3lcore/tiles/Segment.re
index 67a2831eaa..1224901351 100644
--- a/src/haz3lcore/tiles/Segment.re
+++ b/src/haz3lcore/tiles/Segment.re
@@ -123,7 +123,8 @@ and subsort_of = (sort: Sort.t): list(Sort.t) =>
   | Drv(drv) =>
     (
       switch (drv) {
-      | Jdmt => [Prop, Exp, Pat, Typ, TPat]
+      | Jdmt => [Ctxt, Prop, Exp, Pat, Typ, TPat]
+      | Ctxt => [Prop, Exp, Pat, Typ, TPat]
       | Prop => [Exp, Pat, Typ, TPat]
       | Exp => [Pat, Typ, TPat]
       | Pat => [Typ]
diff --git a/src/haz3lweb/explainthis/data/DeductionExp.re b/src/haz3lweb/explainthis/data/DeductionExp.re
index 33ff58325e..3334113858 100644
--- a/src/haz3lweb/explainthis/data/DeductionExp.re
+++ b/src/haz3lweb/explainthis/data/DeductionExp.re
@@ -105,7 +105,7 @@ let rec repr = (p: int, prop: t, ~color_map: ColorSteps.t): list(Node.t) => {
     | Unroll(a) => repr_aba_tight(["unroll(", ")"], [a])
     | TPat(x) => x |> mk
     | Pat(x) => x |> mk
-    | HasTy(a, b) => repr_binop(":", a, b)
+    | HasType(a, b) => repr_binop(":", a, b)
     | Syn(a, b) => repr_binop("⇒", a, b)
     | Ana(a, b) => repr_binop("⇐", a, b)
     }
diff --git a/src/haz3lweb/view/CursorInspector.re b/src/haz3lweb/view/CursorInspector.re
index e70d69b4d6..11f1934141 100644
--- a/src/haz3lweb/view/CursorInspector.re
+++ b/src/haz3lweb/view/CursorInspector.re
@@ -185,6 +185,7 @@ let drv_view = (status: DrvInfo.t) => {
   | Some(err) =>
     switch (err) {
     | Jdmt(BadToken(token))
+    | Ctxt(BadToken(token))
     | Prop(BadToken(token))
     | Exp(BadToken(token))
     | Pat(BadToken(token))
@@ -192,6 +193,7 @@ let drv_view = (status: DrvInfo.t) => {
     | TPat(BadToken(token)) =>
       div_err([text(Printf.sprintf("\"%s\" isn't a valid token", token))])
     | Jdmt(MultiHole)
+    | Ctxt(MultiHole)
     | Prop(MultiHole)
     | Exp(MultiHole)
     | Pat(MultiHole)