diff --git a/src/haz3lcore/derivation/DrvTerm.re b/src/haz3lcore/derivation/DrvTerm.re
index 08c36cd358..0305ea1ac8 100644
--- a/src/haz3lcore/derivation/DrvTerm.re
+++ b/src/haz3lcore/derivation/DrvTerm.re
@@ -284,7 +284,7 @@ module Drv = {
 
   include TermBase.Drv;
 
-  let of_typ: t => DrvTyp.t =
+  let sort_of: t => Sort.DrvSort.t =
     fun
     | Jdmt(_) => Jdmt
     | Prop(_) => Prop
diff --git a/src/haz3lcore/derivation/DrvTyp.re b/src/haz3lcore/derivation/DrvTyp.re
deleted file mode 100644
index a0de60e51a..0000000000
--- a/src/haz3lcore/derivation/DrvTyp.re
+++ /dev/null
@@ -1,22 +0,0 @@
-// module Prop = Prop;
-// module Rule = Rule;
-// module Base = DerivationBase;
-// module Verify = Verify;
-
-[@deriving (show({with_path: false}), sexp, yojson)]
-type t =
-  | Jdmt
-  | Prop
-  | Exp
-  | Pat
-  | Typ
-  | TPat;
-
-let repr =
-  fun
-  | Jdmt => "Jdmt"
-  | Prop => "Prop"
-  | Exp => "ALFA_Exp"
-  | Pat => "ALFA_Pat"
-  | Typ => "ALFA_Typ"
-  | TPat => "ALFA_TPat";
diff --git a/src/haz3lcore/dynamics/Casts.re b/src/haz3lcore/dynamics/Casts.re
index 37f5bbd83c..23d502e064 100644
--- a/src/haz3lcore/dynamics/Casts.re
+++ b/src/haz3lcore/dynamics/Casts.re
@@ -58,7 +58,7 @@ let rec ground_cases_of = (ty: Typ.t): ground_cases => {
   | Int
   | Float
   | String
-  | Derivation(_)
+  | Term(_)
   | Var(_)
   | Rec(_)
   | Forall(_, {term: Unknown(_), _})
diff --git a/src/haz3lcore/dynamics/DHExp.re b/src/haz3lcore/dynamics/DHExp.re
index cc266cfb71..70909a06eb 100644
--- a/src/haz3lcore/dynamics/DHExp.re
+++ b/src/haz3lcore/dynamics/DHExp.re
@@ -78,7 +78,7 @@ let rec strip_casts =
         | TypAp(_)
         | Undefined
         | If(_)
-        | Derivation(_) => continue(exp)
+        | Term(_) => continue(exp)
         /* Remove casts*/
         | FailedCast(d, _, _)
         | Cast(d, _, _) => strip_casts(d)
@@ -113,7 +113,7 @@ let ty_subst = (s: Typ.t, tpat: TPat.t, exp: t): t => {
             /* Note that we do not have to worry about capture avoidance, since s will always be closed. */
             }
           | Cast(_)
-          | Derivation(_)
+          | Term(_)
           | FixF(_)
           | Fun(_)
           | TypAp(_)
diff --git a/src/haz3lcore/dynamics/Elaborator.re b/src/haz3lcore/dynamics/Elaborator.re
index ed3e016463..965f4f7cef 100644
--- a/src/haz3lcore/dynamics/Elaborator.re
+++ b/src/haz3lcore/dynamics/Elaborator.re
@@ -242,8 +242,7 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => {
     | Bool(_) => uexp |> cast_from(Bool |> Typ.temp)
     | Float(_) => uexp |> cast_from(Float |> Typ.temp)
     | String(_) => uexp |> cast_from(String |> Typ.temp)
-    | Derivation(d) =>
-      uexp |> cast_from(Derivation(Drv.of_typ(d)) |> Typ.temp)
+    | Term(term) => uexp |> cast_from(Term(Any.sort_of(term)) |> Typ.temp)
     | ListLit(es) =>
       let (ds, tys) = List.map(elaborate(m), es) |> ListUtil.unzip;
       let inner_type =
diff --git a/src/haz3lcore/dynamics/FilterMatcher.re b/src/haz3lcore/dynamics/FilterMatcher.re
index ecccf4a05e..1b147f6c0f 100644
--- a/src/haz3lcore/dynamics/FilterMatcher.re
+++ b/src/haz3lcore/dynamics/FilterMatcher.re
@@ -214,8 +214,8 @@ let rec matches_exp =
     | (String(dv), String(fv)) => dv == fv
     | (String(_), _) => false
 
-    | (Derivation(d), Derivation(f)) => d == f
-    | (Derivation(_), _) => false
+    | (Term(d), Term(f)) => d == f
+    | (Term(_), _) => false
 
     | (
         Constructor(_),
diff --git a/src/haz3lcore/dynamics/Substitution.re b/src/haz3lcore/dynamics/Substitution.re
index 9418a9caa4..6290b37769 100644
--- a/src/haz3lcore/dynamics/Substitution.re
+++ b/src/haz3lcore/dynamics/Substitution.re
@@ -64,7 +64,7 @@ let rec subst_var = (m, d1: DHExp.t, x: Var.t, d2: DHExp.t): DHExp.t => {
   | Int(_)
   | Float(_)
   | String(_)
-  | Derivation(_)
+  | Term(_)
   | Constructor(_) => d2
   | ListLit(ds) => ListLit(List.map(subst_var(m, d1, x), ds)) |> rewrap
   | Cons(d3, d4) =>
diff --git a/src/haz3lcore/dynamics/Transition.re b/src/haz3lcore/dynamics/Transition.re
index e395d68096..31e182ccce 100644
--- a/src/haz3lcore/dynamics/Transition.re
+++ b/src/haz3lcore/dynamics/Transition.re
@@ -290,7 +290,7 @@ module Transition = (EV: EV_MODE) => {
             };
           let+ e =
             switch (DHExp.term_of(d)) {
-            | Derivation(Prop(e)) => Ok(e)
+            | Term(Drv(Prop(e))) => Ok(e)
             | _ => Error("Pat Not Prop type")
             };
           e |> IdTagged.unwrap |> fst;
@@ -347,7 +347,7 @@ module Transition = (EV: EV_MODE) => {
             };
           let+ e =
             switch (DHExp.term_of(d)) {
-            | Derivation(Exp(e)) => Ok(e)
+            | Term(Drv(Exp(e))) => Ok(e)
             | _ => Error("Pat Not ALFA_Exp type")
             };
           e |> IdTagged.unwrap |> fst;
@@ -358,9 +358,9 @@ module Transition = (EV: EV_MODE) => {
     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(Drv(Jdmt(jdmt))) => Term(Drv(Jdmt(go_jdmt(jdmt))))
+      | Term(Drv(Prop(prop))) => Term(Drv(Prop(go_prop(prop))))
+      | Term(Drv(Exp(exp))) => Term(Drv(Exp(go_exp(exp))))
       | _ => term
       };
     term |> rewrap;
@@ -659,7 +659,7 @@ module Transition = (EV: EV_MODE) => {
     | BuiltinFun(_) =>
       let. _ = otherwise(env, d);
       Constructor;
-    | Derivation(_) =>
+    | Term(_) =>
       let. _ = otherwise(env, d);
       let d' = replace_drv_abbrs(env, d);
       if (DHExp.fast_equal(d, d')) {
diff --git a/src/haz3lcore/dynamics/TypeAssignment.re b/src/haz3lcore/dynamics/TypeAssignment.re
index 0352473bcd..bebac7b9b5 100644
--- a/src/haz3lcore/dynamics/TypeAssignment.re
+++ b/src/haz3lcore/dynamics/TypeAssignment.re
@@ -226,7 +226,7 @@ and typ_of_dhexp = (ctx: Ctx.t, m: Statics.Map.t, dh: DHExp.t): option(Typ.t) =>
   | Int(_) => Some(Int |> Typ.temp)
   | Float(_) => Some(Float |> Typ.temp)
   | String(_) => Some(String |> Typ.temp)
-  | Derivation(d) => Some(Derivation(Drv.of_typ(d)) |> Typ.temp)
+  | Term(d) => Some(Term(Any.sort_of(d)) |> Typ.temp)
   | BinOp(Bool(_), d1, d2) =>
     let* ty1 = typ_of_dhexp(ctx, m, d1);
     let* ty2 = typ_of_dhexp(ctx, m, d2);
diff --git a/src/haz3lcore/dynamics/Unboxing.re b/src/haz3lcore/dynamics/Unboxing.re
index 0c6b48e731..5a2f5be6e7 100644
--- a/src/haz3lcore/dynamics/Unboxing.re
+++ b/src/haz3lcore/dynamics/Unboxing.re
@@ -145,8 +145,7 @@ let rec unbox: type a. (unbox_request(a), DHExp.t) => unboxed(a) =
        in elaboration or in the cast calculus. */
     | (
         _,
-        Bool(_) | Int(_) | Float(_) | String(_) | Derivation(_) |
-        Constructor(_) |
+        Bool(_) | Int(_) | Float(_) | String(_) | Term(_) | Constructor(_) |
         BuiltinFun(_) |
         Deferral(_) |
         DeferredAp(_) |
diff --git a/src/haz3lcore/lang/term/Typ.re b/src/haz3lcore/lang/term/Typ.re
index 2986875b53..e31a27ef9a 100644
--- a/src/haz3lcore/lang/term/Typ.re
+++ b/src/haz3lcore/lang/term/Typ.re
@@ -12,7 +12,7 @@ type cls =
   | Float
   | Bool
   | String
-  | Derivation
+  | Term
   | Arrow
   | Prod
   | Sum
@@ -52,7 +52,7 @@ let cls_of_term: term => cls =
   | Float => Float
   | Bool => Bool
   | String => String
-  | Derivation(_) => Derivation
+  | Term(_) => Term
   | List(_) => List
   | Arrow(_) => Arrow
   | Var(_) => Var
@@ -73,8 +73,8 @@ let show_cls: cls => string =
   | Int
   | Float
   | String
-  | Derivation
   | Bool => "Base type"
+  | Term => "Term type"
   | Var => "Type variable"
   | Constructor => "Sum constructor"
   | List => "List type"
@@ -95,7 +95,7 @@ let rec is_arrow = (typ: t) => {
   | Float
   | Bool
   | String
-  | Derivation(_)
+  | Term(_)
   | List(_)
   | Prod(_)
   | Var(_)
@@ -115,7 +115,7 @@ let rec is_forall = (typ: t) => {
   | Float
   | Bool
   | String
-  | Derivation(_)
+  | Term(_)
   | Arrow(_)
   | List(_)
   | Prod(_)
@@ -160,7 +160,7 @@ let rec free_vars = (~bound=[], ty: t): list(Var.t) =>
   | Int
   | Float
   | Bool
-  | Derivation(_)
+  | Term(_)
   | String => []
   | Ap(t1, t2) => free_vars(~bound, t1) @ free_vars(~bound, t2)
   | Var(v) => List.mem(v, bound) ? [] : [v]
@@ -262,8 +262,8 @@ let rec join = (~resolve=false, ~fix, ctx: Ctx.t, ty1: t, ty2: t): option(t) =>
   | (Bool, _) => None
   | (String, String) => Some(ty1)
   | (String, _) => None
-  | (Derivation(d1), Derivation(d2)) when d1 == d2 => Some(ty1)
-  | (Derivation(_), _) => None
+  | (Term(d1), Term(d2)) when d1 == d2 => Some(ty1)
+  | (Term(_), _) => None
   | (Arrow(ty1, ty2), Arrow(ty1', ty2')) =>
     let* ty1 = join'(ty1, ty1');
     let+ ty2 = join'(ty2, ty2');
@@ -299,7 +299,7 @@ let rec match_synswitch = (t1: t, t2: t) => {
   | (Float, _)
   | (Bool, _)
   | (String, _)
-  | (Derivation(_), _)
+  | (Term(_), _)
   | (Var(_), _)
   | (Ap(_), _)
   | (Rec(_), _)
@@ -356,7 +356,7 @@ let rec normalize = (ctx: Ctx.t, ty: t): t => {
   | Int
   | Float
   | Bool
-  | Derivation(_)
+  | Term(_)
   | String => ty
   | Parens(t) => Parens(normalize(ctx, t)) |> rewrap
   | List(t) => List(normalize(ctx, t)) |> rewrap
@@ -487,7 +487,7 @@ let rec needs_parens = (ty: t): bool =>
   | Int
   | Float
   | String
-  | Derivation(_)
+  | Term(_)
   | Bool
   | Var(_) => false
   | Rec(_, _)
@@ -516,7 +516,7 @@ let rec pretty_print = (ty: t): string =>
   | Float => "Float"
   | Bool => "Bool"
   | String => "String"
-  | Derivation(d) => DrvTyp.repr(d)
+  | Term(d) => Sort.to_string(d)
   | Var(tvar) => tvar
   | List(t) => "[" ++ pretty_print(t) ++ "]"
   | Arrow(t1, t2) => paren_pretty_print(t1) ++ " -> " ++ pretty_print(t2)
diff --git a/src/haz3lcore/statics/MakeTerm.re b/src/haz3lcore/statics/MakeTerm.re
index 323b4f00b5..837b505115 100644
--- a/src/haz3lcore/statics/MakeTerm.re
+++ b/src/haz3lcore/statics/MakeTerm.re
@@ -389,7 +389,7 @@ and exp = unsorted => {
     let (term, inner_ids) = jdmt_term(unsorted);
     let ids = ids(unsorted) @ inner_ids;
     let jdmt = return(e => Drv(Jdmt(e)), ids, {ids, copied: false, term});
-    TermBase.Exp.Derivation(Jdmt(jdmt)) |> IdTagged.fresh;
+    TermBase.Exp.Term(Drv(Jdmt(jdmt))) |> IdTagged.fresh;
   | _ =>
     let ids = ids(unsorted) @ inner_ids;
     return(e => Exp(e), ids, {ids, copied: false, term});
@@ -427,13 +427,13 @@ 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_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(Derivation(TPat(tp)))
-      | (["of_Prop", "end"], [Drv(Prop(p))]) => ret(Derivation(Prop(p)))
-      | (["of_Jdmt", "end"], [Drv(Jdmt(j))]) => ret(Derivation(Jdmt(j)))
+        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))))
       | ([t], []) when t != " " && !Form.is_explicit_hole(t) =>
         ret(Invalid(t))
       | _ => ret(hole(tm))
@@ -463,9 +463,9 @@ and exp_term: unsorted => (UExp.term, list(Id.t)) = {
         | (["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)
+          Let(pat, UExp.Term(Drv(Prop(def))) |> UExp.fresh, r)
         | (["alfa", "=", "in"], [Pat(pat), Drv(Exp(def))]) =>
-          Let(pat, UExp.Derivation(Exp(def)) |> UExp.fresh, r)
+          Let(pat, UExp.Term(Drv(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 77b520131d..f3fd9a5534 100644
--- a/src/haz3lcore/statics/Statics.re
+++ b/src/haz3lcore/statics/Statics.re
@@ -226,7 +226,7 @@ and drv_to_info_map =
            ~co_ctx=CoCtx.empty,
            ~ctx,
            ~ancestors,
-           ~mode=Mode.Ana(Derivation(DrvTyp.Prop) |> Typ.fresh),
+           ~mode=Mode.Ana(Term(Drv(Prop)) |> Typ.fresh),
            p,
          )
       |> snd
@@ -295,7 +295,7 @@ and drv_to_info_map =
            ~co_ctx=CoCtx.empty,
            ~ctx,
            ~ancestors,
-           ~mode=Mode.Ana(Derivation(DrvTyp.Prop) |> Typ.fresh),
+           ~mode=Mode.Ana(Term(Drv(Exp)) |> Typ.fresh),
            p,
          )
       |> snd
@@ -428,10 +428,10 @@ and uexp_to_info_map =
   | Int(_) => atomic(Just(Int |> Typ.temp))
   | Float(_) => atomic(Just(Float |> Typ.temp))
   | String(_) => atomic(Just(String |> Typ.temp))
-  | Derivation(d) =>
-    let m = drv_to_info_map(d, m, ~ancestors, ~ctx) |> snd;
+  | Term(term) =>
+    let m = any_to_info_map(term, m, ~ancestors, ~ctx) |> snd;
     add(
-      ~self=Just(Derivation(Drv.of_typ(d)) |> Typ.temp),
+      ~self=Just(Term(Any.sort_of(term)) |> Typ.temp),
       ~co_ctx=CoCtx.empty,
       m,
     );
@@ -1045,7 +1045,7 @@ and utyp_to_info_map =
   | Int
   | Float
   | Bool
-  | Derivation(_)
+  | Term(_)
   | String => add(m)
   | Var(_) =>
     /* Names are resolved in Info.status_typ */
diff --git a/src/haz3lcore/statics/Term.re b/src/haz3lcore/statics/Term.re
index b2472ba5fb..0d19bc4835 100644
--- a/src/haz3lcore/statics/Term.re
+++ b/src/haz3lcore/statics/Term.re
@@ -319,7 +319,7 @@ module Exp = {
     | BuiltinFun
     | Match
     | Cast
-    | Derivation
+    | Term
     | ListConcat;
 
   let hole = (tms: list(TermBase.Any.t)): term =>
@@ -370,7 +370,7 @@ module Exp = {
     | BuiltinFun(_) => BuiltinFun
     | Match(_) => Match
     | Cast(_) => Cast
-    | Derivation(_) => Derivation;
+    | Term(_) => Term;
 
   let show_cls: cls => string =
     fun
@@ -414,7 +414,7 @@ module Exp = {
     | BuiltinFun => "Built-in Function"
     | Match => "Case expression"
     | Cast => "Cast expression"
-    | Derivation => "Cast derivation sort";
+    | Term => "Term expression";
 
   // Typfun should be treated as a function here as this is only used to
   // determine when to allow for recursive definitions in a let binding.
@@ -456,7 +456,7 @@ module Exp = {
     | BinOp(_)
     | Match(_)
     | Constructor(_)
-    | Derivation(_) => false
+    | Term(_) => false
     };
   };
 
@@ -500,7 +500,7 @@ module Exp = {
       | BinOp(_)
       | Match(_)
       | Constructor(_)
-      | Derivation(_) => false
+      | Term(_) => false
       }
     );
 
@@ -558,7 +558,7 @@ module Exp = {
       | BinOp(_)
       | Match(_)
       | Constructor(_)
-      | Derivation(_) => None
+      | Term(_) => None
       };
     };
 };
@@ -611,6 +611,17 @@ module Any = {
     | Drv(Prop(p)) => Some(p)
     | _ => None;
 
+  let sort_of: t => Sort.t =
+    fun
+    | Any(_) => Any
+    | Exp(_) => Exp
+    | Pat(_) => Pat
+    | Typ(_) => Typ
+    | TPat(_) => TPat
+    | Rul(_) => Rul
+    | Drv(drv) => Drv(DrvTerm.Drv.sort_of(drv))
+    | Nul(_) => Nul;
+
   let rec ids =
     fun
     | Drv(Jdmt(tm)) => tm.ids
diff --git a/src/haz3lcore/statics/TermBase.re b/src/haz3lcore/statics/TermBase.re
index 2cafbe7f3b..69fd37f3d8 100644
--- a/src/haz3lcore/statics/TermBase.re
+++ b/src/haz3lcore/statics/TermBase.re
@@ -92,7 +92,7 @@ module rec Any: {
         x,
       ) => {
     let pat_map_term =
-      Pat.map_term(~f_exp, ~f_pat, ~f_typ, ~f_tpat, ~f_rul, ~f_any);
+      Pat.map_term(~f_exp, ~f_pat, ~f_typ, ~f_tpat, ~f_rul, ~f_any, ~f_drv);
     let rec_call = y =>
       switch (y) {
       | Drv(x) => Drv(Drv.map_term(~f_hazel_pat=pat_map_term, ~f_drv, x))
@@ -111,13 +111,44 @@ module rec Any: {
         )
       | 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))
+        Typ(
+          Typ.map_term(
+            ~f_exp,
+            ~f_pat,
+            ~f_typ,
+            ~f_tpat,
+            ~f_rul,
+            ~f_any,
+            ~f_drv,
+            x,
+          ),
+        )
       | TPat(x) =>
         TPat(
-          TPat.map_term(~f_exp, ~f_pat, ~f_typ, ~f_tpat, ~f_rul, ~f_any, x),
+          TPat.map_term(
+            ~f_exp,
+            ~f_pat,
+            ~f_typ,
+            ~f_tpat,
+            ~f_rul,
+            ~f_any,
+            ~f_drv,
+            x,
+          ),
         )
       | Rul(x) =>
-        Rul(Rul.map_term(~f_exp, ~f_pat, ~f_typ, ~f_tpat, ~f_rul, ~f_any, x))
+        Rul(
+          Rul.map_term(
+            ~f_exp,
+            ~f_pat,
+            ~f_typ,
+            ~f_tpat,
+            ~f_rul,
+            ~f_any,
+            ~f_drv,
+            x,
+          ),
+        )
       | Nul () => Nul()
       | Any () => Any()
       };
@@ -176,6 +207,7 @@ and Exp: {
     | Int(int)
     | Float(float)
     | String(string)
+    | Term(Any.t)
     | ListLit(list(t))
     | Constructor(string, Typ.t) // Typ.t field is only meaningful in dynamic expressions
     | Fun(
@@ -209,7 +241,6 @@ and Exp: {
        two consistent types. Both types should be normalized in
        dynamics for the cast calculus to work right. */
     | Cast(t, Typ.t, Typ.t) // first Typ.t field is only meaningful in dynamic expressions
-    | Derivation(Drv.t)
   and t = IdTagged.t(term);
 
   let map_term:
@@ -245,6 +276,7 @@ and Exp: {
     | Int(int)
     | Float(float)
     | String(string)
+    | Term(Any.t)
     | ListLit(list(t))
     | Constructor(string, Typ.t)
     | Fun(
@@ -275,7 +307,6 @@ and Exp: {
     | BuiltinFun(string) /// Doesn't currently have a distinguishable syntax
     | Match(t, list((Pat.t, t)))
     | Cast(t, Typ.t, Typ.t)
-    | Derivation(Drv.t)
   and t = IdTagged.t(term);
 
   let map_term =
@@ -292,13 +323,13 @@ and Exp: {
     let exp_map_term =
       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);
+      Pat.map_term(~f_exp, ~f_pat, ~f_typ, ~f_tpat, ~f_rul, ~f_any, ~f_drv);
     let typ_map_term =
-      Typ.map_term(~f_exp, ~f_pat, ~f_typ, ~f_tpat, ~f_rul, ~f_any);
+      Typ.map_term(~f_exp, ~f_pat, ~f_typ, ~f_tpat, ~f_rul, ~f_any, ~f_drv);
     let tpat_map_term =
-      TPat.map_term(~f_exp, ~f_pat, ~f_typ, ~f_tpat, ~f_rul, ~f_any);
+      TPat.map_term(~f_exp, ~f_pat, ~f_typ, ~f_tpat, ~f_rul, ~f_any, ~f_drv);
     let any_map_term =
-      Any.map_term(~f_exp, ~f_pat, ~f_typ, ~f_tpat, ~f_rul, ~f_any);
+      Any.map_term(~f_exp, ~f_pat, ~f_typ, ~f_tpat, ~f_rul, ~f_any, ~f_drv);
     let flt_map_term =
       StepperFilterKind.map_term(
         ~f_exp,
@@ -308,7 +339,6 @@ 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:
@@ -363,7 +393,7 @@ and Exp: {
             ),
           )
         | Cast(e, t1, t2) => Cast(exp_map_term(e), t1, t2)
-        | Derivation(e) => Derivation(drv_map_term(e))
+        | Term(e) => Term(any_map_term(e))
         },
     };
     x |> f_exp(rec_call);
@@ -448,7 +478,7 @@ and Exp: {
          )
     | (Cast(e1, t1, t2), Cast(e2, t3, t4)) =>
       fast_equal(e1, e2) && Typ.fast_equal(t1, t3) && Typ.fast_equal(t2, t4)
-    | (Derivation(d1), Derivation(d2)) => Drv.fast_equal(d1, d2)
+    | (Term(t1), Term(t2)) => Any.fast_equal(t1, t2)
     | (Invalid(_), _)
     | (FailedCast(_), _)
     | (Deferral(_), _)
@@ -480,7 +510,7 @@ and Exp: {
     | (BuiltinFun(_), _)
     | (Match(_), _)
     | (Cast(_), _)
-    | (Derivation(_), _)
+    | (Term(_), _)
     | (MultiHole(_), _)
     | (EmptyHole, _)
     | (Undefined, _) => false
@@ -515,6 +545,7 @@ and Pat: {
       ~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_drv: Drv.mapper=?,
       t
     ) =>
     t;
@@ -549,14 +580,15 @@ and Pat: {
         ~f_tpat=continue,
         ~f_rul=continue,
         ~f_any=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);
+      Pat.map_term(~f_exp, ~f_pat, ~f_typ, ~f_tpat, ~f_rul, ~f_any, ~f_drv);
     let typ_map_term =
-      Typ.map_term(~f_exp, ~f_pat, ~f_typ, ~f_tpat, ~f_rul, ~f_any);
+      Typ.map_term(~f_exp, ~f_pat, ~f_typ, ~f_tpat, ~f_rul, ~f_any, ~f_drv);
     let any_map_term =
-      Any.map_term(~f_exp, ~f_pat, ~f_typ, ~f_tpat, ~f_rul, ~f_any);
+      Any.map_term(~f_exp, ~f_pat, ~f_typ, ~f_tpat, ~f_rul, ~f_any, ~f_drv);
     let rec_call = ({term, _} as exp: t) => {
       ...exp,
       term:
@@ -644,7 +676,7 @@ and Typ: {
     | Float
     | Bool
     | String
-    | Derivation(DrvTyp.t)
+    | Term(Sort.t)
     | Var(string)
     | List(t)
     | Arrow(t, t)
@@ -666,6 +698,7 @@ and Typ: {
       ~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_drv: Drv.mapper=?,
       t
     ) =>
     t;
@@ -691,7 +724,7 @@ and Typ: {
     | Float
     | Bool
     | String
-    | Derivation(DrvTyp.t)
+    | Term(Sort.t)
     | Var(string)
     | List(t)
     | Arrow(t, t)
@@ -713,14 +746,15 @@ and Typ: {
         ~f_tpat=continue,
         ~f_rul=continue,
         ~f_any=continue,
+        ~f_drv=Drv.drv_continue,
         x,
       ) => {
     let typ_map_term =
-      Typ.map_term(~f_exp, ~f_pat, ~f_typ, ~f_tpat, ~f_rul, ~f_any);
+      Typ.map_term(~f_exp, ~f_pat, ~f_typ, ~f_tpat, ~f_rul, ~f_any, ~f_drv);
     let any_map_term =
-      Any.map_term(~f_exp, ~f_pat, ~f_typ, ~f_tpat, ~f_rul, ~f_any);
+      Any.map_term(~f_exp, ~f_pat, ~f_typ, ~f_tpat, ~f_rul, ~f_any, ~f_drv);
     let tpat_map_term =
-      TPat.map_term(~f_exp, ~f_pat, ~f_typ, ~f_tpat, ~f_rul, ~f_any);
+      TPat.map_term(~f_exp, ~f_pat, ~f_typ, ~f_tpat, ~f_rul, ~f_any, ~f_drv);
     let rec_call = ({term, _} as exp: t) => {
       ...exp,
       term:
@@ -733,7 +767,7 @@ and Typ: {
         | Int
         | Float
         | String
-        | Derivation(_)
+        | Term(_)
         | Var(_) => term
         | List(t) => List(typ_map_term(t))
         | Unknown(Hole(MultiHole(things))) =>
@@ -769,7 +803,7 @@ and Typ: {
       | Float => Float |> rewrap
       | Bool => Bool |> rewrap
       | String => String |> rewrap
-      | Derivation(d) => Derivation(d) |> rewrap
+      | Term(sort) => Term(sort) |> rewrap
       | Unknown(prov) => Unknown(prov) |> rewrap
       | Arrow(ty1, ty2) =>
         Arrow(subst(s, x, ty1), subst(s, x, ty2)) |> rewrap
@@ -818,8 +852,8 @@ and Typ: {
     | (Bool, _) => false
     | (String, String) => true
     | (String, _) => false
-    | (Derivation(d1), Derivation(d2)) => d1 == d2
-    | (Derivation(_), _) => false
+    | (Term(s1), Term(s2)) => s1 == s2
+    | (Term(_), _) => false
     | (Ap(t1, t2), Ap(t1', t2')) =>
       eq_internal(n, t1, t1') && eq_internal(n, t2, t2')
     | (Ap(_), _) => false
@@ -860,6 +894,7 @@ and TPat: {
       ~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_drv: Drv.mapper=?,
       t
     ) =>
     t;
@@ -884,10 +919,11 @@ and TPat: {
         ~f_tpat=continue,
         ~f_rul=continue,
         ~f_any=continue,
+        ~f_drv=Drv.drv_continue,
         x,
       ) => {
     let any_map_term =
-      Any.map_term(~f_exp, ~f_pat, ~f_typ, ~f_tpat, ~f_rul, ~f_any);
+      Any.map_term(~f_exp, ~f_pat, ~f_typ, ~f_tpat, ~f_rul, ~f_any, ~f_drv);
     let rec_call = ({term, _} as exp: t) => {
       ...exp,
       term:
@@ -937,6 +973,7 @@ and Rul: {
       ~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_drv: Drv.mapper=?,
       t
     ) =>
     t;
@@ -958,14 +995,15 @@ and Rul: {
         ~f_tpat=continue,
         ~f_rul=continue,
         ~f_any=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);
+      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);
+      Pat.map_term(~f_exp, ~f_pat, ~f_typ, ~f_tpat, ~f_rul, ~f_any, ~f_drv);
     let any_map_term =
-      Any.map_term(~f_exp, ~f_pat, ~f_typ, ~f_tpat, ~f_rul, ~f_any);
+      Any.map_term(~f_exp, ~f_pat, ~f_typ, ~f_tpat, ~f_rul, ~f_any, ~f_drv);
     let rec_call = ({term, _} as exp: t) => {
       ...exp,
       term:
@@ -1152,6 +1190,7 @@ and StepperFilterKind: {
       ~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_drv: Drv.mapper=?,
       t
     ) =>
     t;
@@ -1186,9 +1225,10 @@ and StepperFilterKind: {
         ~f_tpat=continue,
         ~f_rul=continue,
         ~f_any=continue,
+        ~f_drv=Drv.drv_continue,
       ) => {
     let exp_map_term =
-      Exp.map_term(~f_exp, ~f_pat, ~f_typ, ~f_tpat, ~f_rul, ~f_any);
+      Exp.map_term(~f_exp, ~f_pat, ~f_typ, ~f_tpat, ~f_rul, ~f_any, ~f_drv);
     fun
     | Filter({pat: e, act}) => Filter({pat: exp_map_term(e), act})
     | Residue(i, a) => Residue(i, a);
diff --git a/src/haz3lcore/zipper/Ancestors.re b/src/haz3lcore/zipper/Ancestors.re
index 2acc7d0838..148af95c31 100644
--- a/src/haz3lcore/zipper/Ancestors.re
+++ b/src/haz3lcore/zipper/Ancestors.re
@@ -13,9 +13,9 @@ let parent: t => option(Ancestor.t) =
   | [] => None
   | [(parent, _), ..._] => Some(parent);
 
-let sort =
+let sort = (~root: Sort.t) =>
   fun
-  | [] => Sort.root
+  | [] => root
   | [(a, _), ..._] => Ancestor.sort(a);
 
 let zip_gen = (seg: Segment.t, (a, (pre, suf)): generation): Segment.t =>
diff --git a/src/haz3lcore/zipper/Editor.re b/src/haz3lcore/zipper/Editor.re
index cd05476fd9..8624dbd0ea 100644
--- a/src/haz3lcore/zipper/Editor.re
+++ b/src/haz3lcore/zipper/Editor.re
@@ -89,11 +89,17 @@ module Meta = {
     col_target: int,
     statics: CachedStatics.t,
     syntax: CachedSyntax.t,
+    sort: Sort.t,
   };
 
-  let init = (~settings: CoreSettings.t, z: Zipper.t) => {
+  let init = (~sort: Sort.t, ~settings: CoreSettings.t, z: Zipper.t) => {
     let statics = CachedStatics.init(~settings, z);
-    {col_target: 0, statics, syntax: CachedSyntax.init(z, statics.info_map)};
+    {
+      col_target: 0,
+      statics,
+      syntax: CachedSyntax.init(z, statics.info_map),
+      sort,
+    };
   };
 
   module type S = {
@@ -124,7 +130,7 @@ module Meta = {
       | Select(Resize(Local(Up | Down))) => meta.col_target
       | _ => (Zipper.caret_point(syntax.measured))(. z).col
       };
-    {col_target, syntax, statics};
+    {col_target, syntax, statics, sort: meta.sort};
   };
 };
 
@@ -136,9 +142,9 @@ module State = {
     meta: Meta.t,
   };
 
-  let init = (zipper, ~settings: CoreSettings.t) => {
+  let init = (~sort: Sort.t, zipper, ~settings: CoreSettings.t) => {
     zipper,
-    meta: Meta.init(zipper, ~settings),
+    meta: Meta.init(~sort, zipper, ~settings),
   };
 
   let next = (~settings: CoreSettings.t, a: Action.t, z: Zipper.t, state) => {
@@ -168,8 +174,8 @@ type t = {
   read_only: bool,
 };
 
-let init = (~read_only=false, z, ~settings: CoreSettings.t) => {
-  state: State.init(z, ~settings),
+let init = (~sort: Sort.t, ~read_only=false, z, ~settings: CoreSettings.t) => {
+  state: State.init(z, ~settings, ~sort),
   history: History.empty,
   read_only,
 };
diff --git a/src/haz3lcore/zipper/EditorUtil.re b/src/haz3lcore/zipper/EditorUtil.re
index 80f03a05c4..b2d8e9a766 100644
--- a/src/haz3lcore/zipper/EditorUtil.re
+++ b/src/haz3lcore/zipper/EditorUtil.re
@@ -32,7 +32,7 @@ let rec append_exp = (e1: Exp.t, e2: Exp.t): Exp.t => {
     | BinOp(_)
     | BuiltinFun(_)
     | Cast(_)
-    | Derivation(_)
+    | Term(_)
     | Match(_) => Exp.{ids: [Id.mk()], copied: false, term: Seq(e1, e2)}
     | Seq(e11, e12) =>
       let e12' = append_exp(e12, e2);
diff --git a/src/haz3lcore/zipper/PersistentZipper.re b/src/haz3lcore/zipper/PersistentZipper.re
index a1bbc094d2..519e7007e2 100644
--- a/src/haz3lcore/zipper/PersistentZipper.re
+++ b/src/haz3lcore/zipper/PersistentZipper.re
@@ -13,13 +13,13 @@ let persist = (zipper: Zipper.t) => {
   };
 };
 
-let unpersist = (persisted: t) =>
+let unpersist = (persisted: t, ~root) =>
   try(Sexplib.Sexp.of_string(persisted.zipper) |> Zipper.t_of_sexp) {
   | _ =>
     print_endline(
       "Warning: using backup text! Serialization may be for an older version of Hazel.",
     );
-    switch (Printer.zipper_of_string(persisted.backup_text)) {
+    switch (Printer.zipper_of_string(persisted.backup_text, ~root)) {
     | None => Zipper.init()
     | Some(z) => z
     };
diff --git a/src/haz3lcore/zipper/Printer.re b/src/haz3lcore/zipper/Printer.re
index e6af6911ec..66bb196da3 100644
--- a/src/haz3lcore/zipper/Printer.re
+++ b/src/haz3lcore/zipper/Printer.re
@@ -89,10 +89,10 @@ let to_string_selection = (editor: Editor.t): string =>
   |> String.concat("\n");
 
 let zipper_of_string =
-    (~zipper_init=Zipper.init(), str: string): option(Zipper.t) => {
+    (~zipper_init=Zipper.init(), str: string, ~root): option(Zipper.t) => {
   let insert = (z: option(Zipper.t), c: string): option(Zipper.t) => {
     let* z = z;
-    try(c == "\r" ? Some(z) : Insert.go(c, z)) {
+    try(c == "\r" ? Some(z) : Insert.go(c, z, ~root)) {
     | exn =>
       print_endline("WARN: zipper_of_string: " ++ Printexc.to_string(exn));
       None;
@@ -104,5 +104,5 @@ let zipper_of_string =
 /* This serializes the current editor to text, resets the current
    editor, and then deserializes. It is intended as a (tactical)
    nuclear option for weird backpack states */
-let reparse = z =>
-  zipper_of_string(~zipper_init=Zipper.init(), zipper_to_string(z));
+let reparse = (z, ~root) =>
+  zipper_of_string(~zipper_init=Zipper.init(), zipper_to_string(z), ~root);
diff --git a/src/haz3lcore/zipper/Relatives.re b/src/haz3lcore/zipper/Relatives.re
index 251cdbc4e9..0f28a4cdf2 100644
--- a/src/haz3lcore/zipper/Relatives.re
+++ b/src/haz3lcore/zipper/Relatives.re
@@ -64,8 +64,8 @@ let delete_parent = ({siblings, ancestors}: t): t => {
   };
 };
 
-let remold = ({siblings, ancestors}: t): t => {
-  let s = Ancestors.sort(ancestors);
+let remold = (~root: Sort.t, {siblings, ancestors}: t): t => {
+  let s = Ancestors.sort(ancestors, ~root);
   let siblings = Siblings.remold(siblings, s);
   {ancestors, siblings};
 };
diff --git a/src/haz3lcore/zipper/Zipper.re b/src/haz3lcore/zipper/Zipper.re
index 958dec4f20..4bc229fb0d 100644
--- a/src/haz3lcore/zipper/Zipper.re
+++ b/src/haz3lcore/zipper/Zipper.re
@@ -118,12 +118,13 @@ let regrout = (d: Direction.t, z: t): t => {
   {...z, relatives};
 };
 
-let remold = (z: t): t => {
+let remold = (~root, z: t): t => {
   assert(Selection.is_empty(z.selection));
-  {...z, relatives: Relatives.remold(z.relatives)};
+  {...z, relatives: Relatives.remold(z.relatives, ~root)};
 };
 
-let remold_regrout = (d: Direction.t, z: t): t => z |> remold |> regrout(d);
+let remold_regrout = (d: Direction.t, z: t, ~root): t =>
+  z |> remold(~root) |> regrout(d);
 
 let clear_unparsed_buffer = (z: t) =>
   switch (z.selection.mode) {
diff --git a/src/haz3lcore/zipper/action/Insert.re b/src/haz3lcore/zipper/action/Insert.re
index d1cbca001f..a59de12f8d 100644
--- a/src/haz3lcore/zipper/action/Insert.re
+++ b/src/haz3lcore/zipper/action/Insert.re
@@ -129,13 +129,13 @@ let insert_outer = (char: string, z as state: t): option(t) =>
   | AppendRight(t) => replace_tile(t, Right, state)
   };
 
-let insert_duo = (lbl: Label.t, z: option(t)): option(t) =>
+let insert_duo = (lbl: Label.t, z: option(t), ~root): option(t) =>
   z
   |> Option.map(z => Zipper.construct(~caret=Left, ~backpack=Left, lbl, z))
   |> OptUtil.and_then(z => {
        //NOTE: regrout to put e.g. ap(1|) back together
        z
-       |> remold_regrout(Left)
+       |> remold_regrout(Left, ~root)
        |> Zipper.put_down(Left)
        |> OptUtil.and_then(Zipper.move(Left))
      });
@@ -145,7 +145,7 @@ let insert_monos = (l: Token.t, r: Token.t, z: option(t)): option(t) =>
   |> Option.map(Zipper.construct_mono(Right, r))
   |> Option.map(Zipper.construct_mono(Left, l));
 
-let split = (z: t, char: string, idx: int, t: Token.t): option(t) => {
+let split = (z: t, char: string, idx: int, t: Token.t, ~root): option(t) => {
   /* Current this necessarily creates three tokens; two from splitting
    * the existing one, and a new one. The two splitting tokens may become
    * delimiters of the same time (e.g. `[|]`=>`[<>|]`). In the future it
@@ -159,14 +159,14 @@ let split = (z: t, char: string, idx: int, t: Token.t): option(t) => {
   |> (
     /* overwrite selection */
     switch (Form.duomerges([l, r])) {
-    | Some(_) => insert_duo([l, r])
+    | Some(_) => insert_duo([l, r], ~root)
     | None => insert_monos(l, r)
     }
   )
   |> OptUtil.and_then(expand_neighbors_and_make_new_tile(char));
 };
 
-let opt_regrold = d => Option.map(remold_regrout(d));
+let opt_regrold = (d, ~root) => Option.map(remold_regrout(d, ~root));
 
 let move_into_if_stringlit_or_comment = (char, z) =>
   /* This is special-case logic for advancing the caret to position between the quotes
@@ -188,9 +188,11 @@ let closing_stringlit_or_comment = (char, t) =>
   && Form.is_comment_delim(char);
 
 let go =
-    (char: string, {caret, relatives: {siblings, _}, _} as z: t): option(t) => {
+    (char: string, {caret, relatives: {siblings, _}, _} as z: t, ~root)
+    : option(t) => {
   /* If there's a selection, delete it before proceeding */
   let z = z.selection.content != [] ? Zipper.destruct(z) : z;
+  print_endline("before go: " ++ Zipper.show(z));
   switch (caret, neighbor_monotiles(siblings)) {
   /* If we try to insert a quote inside an existing string, or a #
    * in a comment, we are instead moved to the righthand side of
@@ -215,8 +217,8 @@ let go =
       ? z
         |> Zipper.set_caret(Inner(d_idx, idx))
         |> Zipper.replace_mono(Right, new_t)
-        |> opt_regrold(Left)
-      : split(z, char, idx, t) |> opt_regrold(Right);
+        |> opt_regrold(Left, ~root)
+      : split(z, char, idx, t, ~root) |> opt_regrold(Right, ~root);
   /* Can't insert inside delimiter */
   | (Inner(_, _), (_, None)) => None
   | (Outer, (_, Some(_))) =>
@@ -232,12 +234,12 @@ let go =
     z
     |> insert_outer(char)
     |> Option.map(Zipper.set_caret(caret))
-    |> opt_regrold(Left)
+    |> opt_regrold(Left, ~root)
     |> Option.map(move_into_if_stringlit_or_comment(char));
   | (Outer, (_, None)) =>
     z
     |> insert_outer(char)
-    |> opt_regrold(Left)
+    |> opt_regrold(Left, ~root)
     |> Option.map(move_into_if_stringlit_or_comment(char))
   };
 };
diff --git a/src/haz3lcore/zipper/action/Perform.re b/src/haz3lcore/zipper/action/Perform.re
index 5a3b90c245..2ebd86ecdf 100644
--- a/src/haz3lcore/zipper/action/Perform.re
+++ b/src/haz3lcore/zipper/action/Perform.re
@@ -19,12 +19,18 @@ let go_z =
       ~settings: CoreSettings.t,
       a: Action.t,
       z: Zipper.t,
+      ~root,
     )
     : Action.Result.t(Zipper.t) => {
   let meta =
     switch (meta) {
     | Some(m) => m
-    | None => Editor.Meta.init(z, ~settings)
+    | None =>
+      Editor.Meta.init(
+        z,
+        ~settings,
+        ~sort=Ancestors.sort(z.relatives.ancestors, ~root),
+      )
     };
   module M = (val Editor.Meta.module_of_t(meta));
   module Move = Move.Make(M);
@@ -32,14 +38,14 @@ let go_z =
 
   let paste = (z: Zipper.t, str: string): option(Zipper.t) => {
     open Util.OptUtil.Syntax;
-    let* z = Printer.zipper_of_string(~zipper_init=z, str);
+    let* z = Printer.zipper_of_string(~zipper_init=z, str, ~root);
     /* HACK(andrew): Insert/Destruct below is a hack to deal
        with the fact that pasting something like "let a = b in"
        won't trigger the barfing of the "in"; to trigger this,
        we insert a space, and then we immediately delete it */
-    let* z = Insert.go(" ", z);
+    let* z = Insert.go(" ", z, ~root);
     let+ z = Destruct.go(Left, z);
-    remold_regrout(Left, z);
+    remold_regrout(Left, z, ~root);
   };
 
   let buffer_accept = (z): option(Zipper.t) =>
@@ -99,7 +105,7 @@ let go_z =
      * This doesn't change state but is included here for logging purposes */
     Ok(z)
   | Reparse =>
-    switch (Printer.reparse(z)) {
+    switch (Printer.reparse(z, ~root)) {
     | None => Error(CantReparse)
     | Some(z) => Ok(z)
     }
@@ -179,15 +185,15 @@ let go_z =
   | Destruct(d) =>
     z
     |> Destruct.go(d)
-    |> Option.map(remold_regrout(d))
+    |> Option.map(remold_regrout(d, ~root))
     |> Result.of_option(~error=Action.Failure.Cant_destruct)
   | Insert(char) =>
     z
-    |> Insert.go(char)
+    |> Insert.go(char, ~root)
     /* note: remolding here is done case-by-case */
     //|> Option.map((z) => remold_regrout(Right, z))
     |> Result.of_option(~error=Action.Failure.Cant_insert)
-  | Pick_up => Ok(remold_regrout(Left, Zipper.pick_up(z)))
+  | Pick_up => Ok(remold_regrout(Left, Zipper.pick_up(z), ~root))
   | Put_down =>
     let z =
       /* Alternatively, putting down inside token could eiter merge-in or split */
@@ -196,7 +202,7 @@ let go_z =
       | Outer => Zipper.put_down(Left, z)
       };
     z
-    |> Option.map(remold_regrout(Left))
+    |> Option.map(remold_regrout(Left, ~root))
     |> Result.of_option(~error=Action.Failure.Cant_put_down);
   | RotateBackpack =>
     let z = {...z, backpack: Util.ListUtil.rotate(z.backpack)};
@@ -221,7 +227,7 @@ let go_history =
   open Result.Syntax;
   /* This function records action history */
   let Editor.State.{zipper, meta} = ed.state;
-  let+ z = go_z(~settings, ~meta, a, zipper);
+  let+ z = go_z(~settings, ~meta, a, zipper, ~root=meta.sort);
   Editor.new_state(~settings, a, z, ed);
 };
 
diff --git a/src/haz3lschool/Exercise.re b/src/haz3lschool/Exercise.re
index ac3af89780..40c20dcbdc 100644
--- a/src/haz3lschool/Exercise.re
+++ b/src/haz3lschool/Exercise.re
@@ -94,6 +94,12 @@ module F = (ExerciseEnv: ExerciseEnv) => {
         Programming.ModelUtil.visible_in(pos, instructor_mode)
       | Proof(pos) => Proof.ModelUtil.visible_in(pos, instructor_mode)
       };
+
+    let root_sort = (pos: pos): Sort.t =>
+      switch (pos) {
+      | Programming(pos) => Programming.ModelUtil.root_sort(pos)
+      | Proof(pos) => Proof.ModelUtil.root_sort(pos)
+      };
   };
 
   // Exported Functions
@@ -134,18 +140,24 @@ module F = (ExerciseEnv: ExerciseEnv) => {
   let positioned_editors = state =>
     List.combine(editor_positions(state), editors(state));
 
-  let zipper_of_code = code => {
-    switch (Printer.zipper_of_string(code)) {
+  let zipper_of_code = (code, ~root) => {
+    switch (Printer.zipper_of_string(code, ~root)) {
     | None => failwith("Transition failed.")
     | Some(zipper) => zipper
     };
   };
 
-  let transition: transitionary_spec => spec =
-    s => {...s, model: s.model |> ModelUtil.map(zipper_of_code)};
+  let transition = s => {
+    ...s,
+    model:
+      s.model
+      |> ModelUtil.mapi((pos, m) =>
+           zipper_of_code(~root=ModelUtil.root_sort(pos), m)
+         ),
+  };
 
   let editor_of_serialization = (zipper: Zipper.t, ~settings: CoreSettings.t) =>
-    Editor.init(zipper, ~settings);
+    Editor.init(zipper, ~settings, ~sort=Exp);
 
   let eds_of_spec = (~settings: CoreSettings.t, {model, _}: spec) =>
     model |> ModelUtil.map(editor_of_serialization(~settings));
@@ -199,8 +211,10 @@ module F = (ExerciseEnv: ExerciseEnv) => {
         pos: spec.pos,
         model:
           persistent_state
-          |> ModelUtil.map(z =>
-               z |> PersistentZipper.unpersist |> Editor.init(~settings)
+          |> ModelUtil.mapi((pos, z) =>
+               z
+               |> PersistentZipper.unpersist(~root=ModelUtil.root_sort(pos))
+               |> Editor.init(~settings, ~sort=ModelUtil.root_sort(pos))
              ),
       },
       ~new_mode=instructor_mode,
diff --git a/src/haz3lschool/ProgrammingCore.re b/src/haz3lschool/ProgrammingCore.re
index 51bf6f18ba..c8b7bcf6a9 100644
--- a/src/haz3lschool/ProgrammingCore.re
+++ b/src/haz3lschool/ProgrammingCore.re
@@ -222,6 +222,11 @@ module ModelUtil = {
     },
     syntax_tests: p.syntax_tests,
   };
+
+  let root_sort = (pos: pos): Haz3lcore.Sort.t => {
+    ignore(pos);
+    Exp;
+  };
 };
 
 /* Multiple stitchings are needed for each exercise
diff --git a/src/haz3lschool/ProofCore.re b/src/haz3lschool/ProofCore.re
index 76d03473e5..725f35c217 100644
--- a/src/haz3lschool/ProofCore.re
+++ b/src/haz3lschool/ProofCore.re
@@ -159,6 +159,13 @@ module ModelUtil = {
            )
          ),
   };
+
+  let root_sort = (pos: pos): Haz3lcore.Sort.t =>
+    switch (pos) {
+    | Prelude => Exp
+    | Setup => Exp
+    | Trees(_, _) => Drv(Jdmt)
+    };
 };
 
 // UI functionality
diff --git a/src/haz3lschool/ProofGrade.re b/src/haz3lschool/ProofGrade.re
index 6e026f2a82..2ca13a596e 100644
--- a/src/haz3lschool/ProofGrade.re
+++ b/src/haz3lschool/ProofGrade.re
@@ -72,7 +72,7 @@ module F = (ExerciseEnv: Exercise.ExerciseEnv) => {
         | ResultOk({result, _}) =>
           ignore(rule);
           switch (result) {
-          | BoxedValue({term: Derivation(d), _}) =>
+          | BoxedValue({term: Term(Drv(d)), _}) =>
             Ok({jdmt: DrvElab.elaborate(d), rule})
           | Indet(_) => Error(EvalIndet)
           | _ => Error(EvalIndet)
diff --git a/src/haz3lschool/SyntaxTest.re b/src/haz3lschool/SyntaxTest.re
index 345724a635..8cb9d29631 100644
--- a/src/haz3lschool/SyntaxTest.re
+++ b/src/haz3lschool/SyntaxTest.re
@@ -126,7 +126,7 @@ let rec find_fn =
   | Int(_)
   | Float(_)
   | String(_)
-  | Derivation(_)
+  | Term(_)
   | Constructor(_)
   | Undefined
   | BuiltinFun(_)
@@ -178,7 +178,7 @@ let rec var_mention = (name: string, uexp: Exp.t): bool => {
   | Int(_)
   | Float(_)
   | String(_)
-  | Derivation(_)
+  | Term(_)
   | Constructor(_)
   | Undefined
   | Deferral(_) => false
@@ -240,7 +240,7 @@ let rec var_applied = (name: string, uexp: Exp.t): bool => {
   | Int(_)
   | Float(_)
   | String(_)
-  | Derivation(_)
+  | Term(_)
   | Constructor(_)
   | Undefined
   | Deferral(_) => false
@@ -332,7 +332,7 @@ let rec tail_check = (name: string, uexp: Exp.t): bool => {
   | Int(_)
   | Float(_)
   | String(_)
-  | Derivation(_)
+  | Term(_)
   | Constructor(_)
   | Undefined
   | Var(_)
diff --git a/src/haz3lweb/ScratchSlide.re b/src/haz3lweb/ScratchSlide.re
index 554beab53d..cb4c2fb256 100644
--- a/src/haz3lweb/ScratchSlide.re
+++ b/src/haz3lweb/ScratchSlide.re
@@ -13,8 +13,8 @@ let persist = (editor: Editor.t): persistent_state => {
 };
 
 let unpersist = (zipper: persistent_state, ~settings: CoreSettings.t): state => {
-  let zipper = PersistentZipper.unpersist(zipper);
-  Editor.init(zipper, ~read_only=false, ~settings);
+  let zipper = PersistentZipper.unpersist(zipper, ~root=Exp);
+  Editor.init(zipper, ~read_only=false, ~settings, ~sort=Exp);
 };
 
 let serialize = (state: state): string => {
diff --git a/src/haz3lweb/Store.re b/src/haz3lweb/Store.re
index 52e9f22939..8bcd847019 100644
--- a/src/haz3lweb/Store.re
+++ b/src/haz3lweb/Store.re
@@ -193,8 +193,8 @@ module Documentation = {
   };
 
   let unpersist = ((name, zipper), ~settings: CoreSettings.t) => {
-    let zipper = PersistentZipper.unpersist(zipper);
-    (name, Editor.init(zipper, ~read_only=false, ~settings));
+    let zipper = PersistentZipper.unpersist(zipper, ~root=Exp);
+    (name, Editor.init(zipper, ~read_only=false, ~settings, ~sort=Exp));
   };
 
   let to_persistent = ((string, slides, results)): persistent => (
diff --git a/src/haz3lweb/explainthis/Example.re b/src/haz3lweb/explainthis/Example.re
index e0bc591227..ceb45218c1 100644
--- a/src/haz3lweb/explainthis/Example.re
+++ b/src/haz3lweb/explainthis/Example.re
@@ -130,8 +130,8 @@ let mk_unquote = mk_tile(Form.get("unquote"));
 let linebreak = () => mk_secondary(Form.linebreak);
 let space = () => mk_secondary(Form.space);
 
-let mk_example = str => {
-  switch (Printer.zipper_of_string(str)) {
+let mk_example = (~root=Sort.Exp, str) => {
+  switch (Printer.zipper_of_string(str, ~root)) {
   | None => []
   | Some(z) => Zipper.zip(z)
   };
diff --git a/src/haz3lweb/explainthis/data/TerminalTyp.re b/src/haz3lweb/explainthis/data/TerminalTyp.re
index 134caaefc9..bd43147bb9 100644
--- a/src/haz3lweb/explainthis/data/TerminalTyp.re
+++ b/src/haz3lweb/explainthis/data/TerminalTyp.re
@@ -45,11 +45,11 @@ let str_typ: form = {
   };
 };
 
-let prop_typ: form = {
-  let explanation = "The `Prop` type classifies propositions.";
+let term_typ: form = {
+  let explanation = "The `Term` type classifies terms.";
   {
     id: PropTyp,
-    syntactic_form: [typ("Prop")],
+    syntactic_form: [typ("Term")],
     expandable_id: None,
     explanation,
     examples: [],
@@ -75,6 +75,6 @@ let bool: group = {id: BoolTyp, forms: [bool_typ]};
 
 let str: group = {id: StrTyp, forms: [str_typ]};
 
-let prop: group = {id: PropTyp, forms: [prop_typ]};
+let term: group = {id: PropTyp, forms: [term_typ]};
 
 let var = (name: string): group => {id: VarTyp, forms: [var_typ(name)]};
diff --git a/src/haz3lweb/view/Cell.re b/src/haz3lweb/view/Cell.re
index 65c01e1a6f..207219ee89 100644
--- a/src/haz3lweb/view/Cell.re
+++ b/src/haz3lweb/view/Cell.re
@@ -262,7 +262,7 @@ let editor_view =
       ~footer: option(list(Node.t))=?,
       ~highlights: option(ColorSteps.colorMap),
       ~overlayer: option(Node.t)=None,
-      ~sort=Sort.root,
+      ~sort,
       ~override_statics: option(Editor.CachedStatics.t)=?,
       editor: Editor.t,
     ) => {
@@ -382,7 +382,7 @@ let locked_no_statics =
     ~sort,
     segment
     |> Zipper.unzip
-    |> Editor.init(~settings=CoreSettings.off, ~read_only=true),
+    |> Editor.init(~settings=CoreSettings.off, ~read_only=true, ~sort),
   ),
 ];
 
@@ -396,11 +396,12 @@ let locked =
       ~inject,
       ~target_id,
       ~segment: Segment.t,
+      ~sort,
     ) => {
   let editor =
     segment
     |> Zipper.unzip
-    |> Editor.init(~settings=settings.core, ~read_only=true);
+    |> Editor.init(~settings=settings.core, ~read_only=true, ~sort);
   let statics = editor.state.meta.statics;
   let elab =
     settings.core.elaborate || settings.core.dynamics
@@ -440,6 +441,7 @@ let locked =
     ~target_id,
     ~footer,
     ~test_results=ModelResult.test_results(result),
+    ~sort,
     editor,
   );
 };
diff --git a/src/haz3lweb/view/ExplainThis.re b/src/haz3lweb/view/ExplainThis.re
index 07a50491c4..620ac0a296 100644
--- a/src/haz3lweb/view/ExplainThis.re
+++ b/src/haz3lweb/view/ExplainThis.re
@@ -244,6 +244,7 @@ let expander_deco =
         Editor.Meta.init(
           ~settings=CoreSettings.off,
           Zipper.unzip(doc.syntactic_form),
+          ~sort=Exp,
         );
       let highlights: option(ColorSteps.colorMap) = None;
     });
@@ -378,6 +379,7 @@ let example_view =
                   ~ui_state,
                   ~settings,
                   ~inject,
+                  ~sort=Exp,
                 ),
                 div(
                   ~attrs=[clss(["explanation"])],
@@ -951,7 +953,7 @@ let get_doc =
         | Int(i) => get_message(TerminalExp.int_exps(i))
         | Float(f) => get_message(TerminalExp.float_exps(f))
         | String(s) => get_message(TerminalExp.string_exps(s))
-        | Derivation(_) => get_message(TerminalExp.string_exps("")) // TOOD(zhiyao): DerivationExp.derivation_exps
+        | Term(_) => get_message(TerminalExp.string_exps("")) // TOOD(zhiyao): DerivationExp.derivation_exps
         | ListLit(terms) =>
           get_message(
             ~format=
@@ -2561,7 +2563,7 @@ let get_doc =
       | Float => get_message(TerminalTyp.float)
       | Bool => get_message(TerminalTyp.bool)
       | String => get_message(TerminalTyp.str)
-      | Derivation(_) => get_message(TerminalTyp.prop) // TODO(zhiyao): Add prop to TerminalTyp
+      | Term(_) => get_message(TerminalTyp.term) // TODO(zhiyao): Add prop to TerminalTyp
       | List(elem) =>
         let elem_id = List.nth(elem.ids, 0);
         get_message(
diff --git a/src/haz3lweb/view/ScratchMode.re b/src/haz3lweb/view/ScratchMode.re
index 7fdc8eb361..e1b1540d91 100644
--- a/src/haz3lweb/view/ScratchMode.re
+++ b/src/haz3lweb/view/ScratchMode.re
@@ -39,6 +39,7 @@ let view =
       ~test_results,
       ~footer?,
       ~highlights,
+      ~sort=Exp,
       editor,
     ),
   ];
diff --git a/src/haz3lweb/view/Type.re b/src/haz3lweb/view/Type.re
index 22e96fd519..4a4818b4a9 100644
--- a/src/haz3lweb/view/Type.re
+++ b/src/haz3lweb/view/Type.re
@@ -30,7 +30,7 @@ let rec view_ty = (~strip_outer_parens=false, ty: Haz3lcore.Typ.t): Node.t =>
   | Float => ty_view("Float", "Float")
   | String => ty_view("String", "String")
   | Bool => ty_view("Bool", "Bool")
-  | Derivation(t) => ty_view("Drv", DrvTyp.repr(t))
+  | Term(sort) => ty_view("Term", "Term " ++ Sort.to_string(sort))
   | Var(name) => ty_view("Var", name)
   | Rec(name, t) =>
     div(
diff --git a/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re b/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re
index 8bb20fedaf..cbaffe5dc0 100644
--- a/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re
+++ b/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re
@@ -53,7 +53,7 @@ let rec precedence = (~show_function_bodies, ~show_casts: bool, d: DHExp.t) => {
   | Test(_)
   | Float(_)
   | String(_)
-  | Derivation(_)
+  | Term(_)
   | ListLit(_)
   | EmptyHole
   | Constructor(_)
@@ -320,7 +320,7 @@ let mk =
       | Int(n) => DHDoc_common.mk_IntLit(n)
       | Float(f) => DHDoc_common.mk_FloatLit(f)
       | String(s) => DHDoc_common.mk_StringLit(s)
-      | Derivation(d) => DHDoc_common.mk_DerivationLit(d)
+      | Term(term) => DHDoc_common.mk_Term(term)
       | Undefined => DHDoc_common.mk_Undefined()
       | Test(d) => DHDoc_common.mk_Test(go'(d))
       | Deferral(_) => text("_")
diff --git a/src/haz3lweb/view/dhcode/layout/DHDoc_common.re b/src/haz3lweb/view/dhcode/layout/DHDoc_common.re
index 1c9a0948cc..5cba55a12a 100644
--- a/src/haz3lweb/view/dhcode/layout/DHDoc_common.re
+++ b/src/haz3lweb/view/dhcode/layout/DHDoc_common.re
@@ -102,8 +102,7 @@ let mk_IntLit = n => Doc.text(string_of_int(n));
 
 let mk_StringLit = s => Doc.text(Form.string_quote(s));
 
-let mk_DerivationLit = (t: Drv.t) =>
-  Doc.text(DrvSyntax.repr(DrvElab.elaborate(t)));
+let mk_Term = t => Doc.text(Any.show(t));
 
 let mk_Test = t => Doc.(hcats([text("Test"), t, text("End")]));
 
diff --git a/src/haz3lweb/view/dhcode/layout/DHDoc_common.rei b/src/haz3lweb/view/dhcode/layout/DHDoc_common.rei
index 9766273e55..f0c378d24b 100644
--- a/src/haz3lweb/view/dhcode/layout/DHDoc_common.rei
+++ b/src/haz3lweb/view/dhcode/layout/DHDoc_common.rei
@@ -86,7 +86,7 @@ let mk_ConstructorLit: string => Pretty.Doc.t('a);
 
 let mk_StringLit: string => Pretty.Doc.t('a);
 
-let mk_DerivationLit: Drv.t => Pretty.Doc.t('a);
+let mk_Term: Any.t => Pretty.Doc.t('a);
 
 let mk_Cons: (Pretty.Doc.t('a), Pretty.Doc.t('a)) => Pretty.Doc.t('a);
 
diff --git a/src/haz3lweb/view/dhcode/layout/HTypDoc.re b/src/haz3lweb/view/dhcode/layout/HTypDoc.re
index 22c500a67a..d05d22fa36 100644
--- a/src/haz3lweb/view/dhcode/layout/HTypDoc.re
+++ b/src/haz3lweb/view/dhcode/layout/HTypDoc.re
@@ -18,7 +18,7 @@ let precedence = (ty: Typ.t): int =>
   | Float
   | Bool
   | String
-  | Derivation(_)
+  | Term(_)
   | Unknown(_)
   | Var(_)
   | Forall(_)
@@ -76,7 +76,7 @@ let rec mk = (~parenthesize=false, ~enforce_inline: bool, ty: Typ.t): t => {
     | Float => (text("Float"), parenthesize)
     | Bool => (text("Bool"), parenthesize)
     | String => (text("String"), parenthesize)
-    | Derivation(d) => (text(DrvTyp.repr(d)), parenthesize)
+    | Term(term) => (text(Sort.to_string(term)), parenthesize)
     | Var(name) => (text(name), parenthesize)
     | List(ty) => (
         hcats([
diff --git a/src/haz3lweb/view/exercise/NinjaKeysRules.re b/src/haz3lweb/view/exercise/NinjaKeysRules.re
index 51caa63e59..1d2b0d6be3 100644
--- a/src/haz3lweb/view/exercise/NinjaKeysRules.re
+++ b/src/haz3lweb/view/exercise/NinjaKeysRules.re
@@ -7,8 +7,8 @@ let staged = ref(false);
 
 let init = () =>
   ""
-  |> Exercise.zipper_of_code
-  |> Haz3lcore.Editor.init(~settings=Haz3lcore.CoreSettings.on);
+  |> Exercise.zipper_of_code(~root=Haz3lcore.Sort.Drv(Jdmt))
+  |> Haz3lcore.Editor.init(~settings=Haz3lcore.CoreSettings.on, ~sort=Exp);
 
 let map_model = (f, state: Exercise.state): Exercise.state => {
   ...state,
diff --git a/src/haz3lweb/view/exercise/ProgrammingView.re b/src/haz3lweb/view/exercise/ProgrammingView.re
index ef4f6f4b08..2d8046492d 100644
--- a/src/haz3lweb/view/exercise/ProgrammingView.re
+++ b/src/haz3lweb/view/exercise/ProgrammingView.re
@@ -61,6 +61,7 @@ let programming_view =
       ~target_id=Exercise.show_pos(this_pos),
       ~test_results=ModelResult.test_results(di.result),
       ~footer?,
+      ~sort=Exp,
       editor,
     );
   };
diff --git a/src/haz3lweb/view/exercise/ProofView.re b/src/haz3lweb/view/exercise/ProofView.re
index 670b361f21..b0c03e32df 100644
--- a/src/haz3lweb/view/exercise/ProofView.re
+++ b/src/haz3lweb/view/exercise/ProofView.re
@@ -37,8 +37,10 @@ let proof_view =
       ~stitched_dynamics: stitched(Exercise.DynamicsItem.t),
       ~highlights,
     ) => {
-  let init = () =>
-    "" |> Exercise.zipper_of_code |> Editor.init(~settings=settings.core);
+  let init = (~sort, ()) =>
+    ""
+    |> Exercise.zipper_of_code(~root=sort)
+    |> Editor.init(~settings=settings.core, ~sort);
 
   let map_model = (f, state: Exercise.state): Exercise.state => {
     ...state,
@@ -66,7 +68,11 @@ let proof_view =
               m =>
                 m
                 |> map_model(
-                     Exercise.Proof.add_premise(~pos, ~index, ~init),
+                     Exercise.Proof.add_premise(
+                       ~pos,
+                       ~index,
+                       ~init=init(~sort=Drv(Jdmt)),
+                     ),
                    )
                 |> (m => {...m, pos: make_pos(pos, index)}),
             ),
@@ -175,7 +181,13 @@ let proof_view =
       _ =>
         inject(
           UpdateAction.MapExercise(
-            map_model(Exercise.Proof.switch_rule(~pos, ~rule=None, ~init)),
+            map_model(
+              Exercise.Proof.switch_rule(
+                ~pos,
+                ~rule=None,
+                ~init=init(~sort=Drv(Jdmt)),
+              ),
+            ),
           ),
         ),
       ~tooltip="Cancel Abbreviation",
@@ -388,7 +400,12 @@ let proof_view =
             UpdateAction.MapExercise(
               m =>
                 m
-                |> map_model(Exercise.Proof.add_abbr(~index, ~init))
+                |> map_model(
+                     Exercise.Proof.add_abbr(
+                       ~index,
+                       ~init=init(~sort=Drv(Jdmt)),
+                     ),
+                   )
                 |> (m => {...m, pos: Proof(Trees(index, Value))}),
             ),
           )