diff --git a/src/haz3lcore/derivation/DrvElab.re b/src/haz3lcore/derivation/DrvElab.re
index 4fe10fae3..4fa5d5b1f 100644
--- a/src/haz3lcore/derivation/DrvElab.re
+++ b/src/haz3lcore/derivation/DrvElab.re
@@ -26,6 +26,7 @@ and elab_jdmt: Drv.Exp.t => t =
   }
 and elab_ctxt: Drv.Exp.t => t =
   ctx => {
+    let hole: term = Hole(Drv.Exp.show(ctx));
     let term: term =
       switch (exp_term_of(ctx)) {
       | Hole(s) => Hole(TermBase.TypeHole.show(s))
@@ -37,8 +38,22 @@ and elab_ctxt: Drv.Exp.t => t =
           |> List.concat
           |> List.fold_left(cons_ctx, []),
         )
-      | _ => Hole(Drv.Exp.show(ctx))
+      | Cons(p, ctx) =>
+        switch (IdTagged.term_of(elab_ctxt(ctx))) {
+        | Ctx(ps) => Ctx(cons_ctx(ps, elab_prop(p)))
+        | _ => hole
+        }
+      | Concat(ctx1, ctx2) =>
+        switch (
+          IdTagged.term_of(elab_ctxt(ctx1)),
+          IdTagged.term_of(elab_ctxt(ctx2)),
+        ) {
+        | (Ctx(ps1), Ctx(ps2)) => Ctx(List.fold_left(cons_ctx, ps2, ps1))
+        | _ => hole
+        }
+      | _ => hole
       };
+    print_endline("elab_ctxt" ++ DrvSyntax.show_term(term));
     {...ctx, term};
   }
 and elab_prop: Drv.Exp.t => t =
@@ -127,7 +142,7 @@ and elab_exp: Drv.Exp.t => t =
       | PrjR(e) => PrjR(elab_exp(e))
       | InjL => hole
       | InjR => hole
-      | Case(e, x, e1, y, e2) =>
+      | Case(e, [(x, e1), (y, e2)]) =>
         let e = elab_exp(e);
         let e1 = elab_exp(e1);
         let e2 = elab_exp(e2);
diff --git a/src/haz3lcore/derivation/DrvInfo.re b/src/haz3lcore/derivation/DrvInfo.re
index fab42d8a3..964a6719c 100644
--- a/src/haz3lcore/derivation/DrvInfo.re
+++ b/src/haz3lcore/derivation/DrvInfo.re
@@ -157,7 +157,9 @@ let types_of_exp = (exp: Drv.Exp.t): list(ty_merged) =>
   | Val(_)
   | Eval(_)
   | Entail(_) => [Jdmt]
-  | Ctx(_) => [Ctx]
+  | Ctx(_)
+  | Cons(_)
+  | Concat(_) => [Ctx]
   | HasType(_)
   | Syn(_)
   | Ana(_)
diff --git a/src/haz3lcore/derivation/DrvSyntax.re b/src/haz3lcore/derivation/DrvSyntax.re
index 508d939e6..2c31aa3eb 100644
--- a/src/haz3lcore/derivation/DrvSyntax.re
+++ b/src/haz3lcore/derivation/DrvSyntax.re
@@ -590,11 +590,21 @@ let rec subst_ty: (t, string, t) => t =
 
 let mem_ctx = p => List.exists(eq(p));
 
+// Note(zhiyao): This implementation of cons_ctx is not linear.
 let cons_ctx = (ctx, p) => {
-  let cmp = p' => show(p') <= show(p);
+  let cmp = p' => show(p) < show(p');
+  let eq_key = p' =>
+    switch (IdTagged.term_of(p): term, IdTagged.term_of(p'): term) {
+    | (HasType(a, _), HasType(b, _)) => eq(a, b)
+    | (Syn(a, _), Syn(b, _)) => eq(a, b)
+    | (Ana(a, _), Ana(b, _)) => eq(a, b)
+    | _ => show(p) == show(p')
+    };
   let rec insert =
     fun
     | [] => [p]
-    | [hd, ...tl] => cmp(hd) ? [p, hd, ...tl] : [hd, ...insert(tl)];
+    | [hd, ...tl] when eq_key(hd) => [p, ...tl]
+    | [hd, ...tl] when cmp(hd) => [p, hd, ...tl]
+    | [hd, ...tl] => [hd, ...insert(tl)];
   insert(ctx);
 };
diff --git a/src/haz3lcore/derivation/DrvTerm.re b/src/haz3lcore/derivation/DrvTerm.re
index 7e691171e..b8aabc473 100644
--- a/src/haz3lcore/derivation/DrvTerm.re
+++ b/src/haz3lcore/derivation/DrvTerm.re
@@ -10,6 +10,8 @@ module ALFA_Exp = {
     | Eval
     | Entail
     | Ctx
+    | Cons
+    | Concat
     | HasType
     | Syn
     | Ana
@@ -68,6 +70,8 @@ module ALFA_Exp = {
     | Eval(_) => Eval
     | Entail(_) => Entail
     | Ctx(_) => Ctx
+    | Cons(_) => Cons
+    | Concat(_) => Concat
     | HasType(_) => HasType
     | Syn(_) => Syn
     | Ana(_) => Ana
@@ -102,6 +106,34 @@ module ALFA_Exp = {
     | Unroll => Unroll;
 };
 
+module ALFA_Rul = {
+  [@deriving (show({with_path: false}), sexp, yojson)]
+  type cls =
+    | Hole
+    | Rules;
+
+  include TermBase.ALFA_Rul;
+
+  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
+    | Rules(_, _) => Rules;
+};
+
 module ALFA_Pat = {
   [@deriving (show({with_path: false}), sexp, yojson)]
   type cls =
@@ -218,6 +250,7 @@ module Drv = {
   [@deriving (show({with_path: false}), sexp, yojson)]
   type cls =
     | Exp(ALFA_Exp.cls)
+    | Rul(ALFA_Rul.cls)
     | Pat(ALFA_Pat.cls)
     | Typ(ALFA_Typ.cls)
     | TPat(ALFA_TPat.cls);
@@ -227,6 +260,7 @@ module Drv = {
   let sort_of: t => Sort.DrvSort.t =
     fun
     | Exp(_) => Exp
+    | Rul(_) => Rul
     | Pat(_) => Pat
     | Typ(_) => Typ
     | TPat(_) => TPat;
@@ -234,6 +268,7 @@ module Drv = {
   let rep_id: t => Id.t =
     fun
     | Exp(exp) => ALFA_Exp.rep_id(exp)
+    | Rul(rul) => ALFA_Rul.rep_id(rul)
     | Pat(pat) => ALFA_Pat.rep_id(pat)
     | Typ(typ) => ALFA_Typ.rep_id(typ)
     | TPat(tpat) => ALFA_TPat.rep_id(tpat);
@@ -241,6 +276,7 @@ module Drv = {
   let of_id: t => list(Id.t) =
     fun
     | Exp(exp) => exp.ids
+    | Rul(rul) => rul.ids
     | Pat(pat) => pat.ids
     | Typ(typ) => typ.ids
     | TPat(tpat) => tpat.ids;
@@ -248,6 +284,7 @@ module Drv = {
   let cls_of: t => cls =
     fun
     | Exp(exp) => Exp(ALFA_Exp.cls_of_term(exp.term))
+    | Rul(rul) => Rul(ALFA_Rul.cls_of_term(rul.term))
     | Pat(pat) => Pat(ALFA_Pat.cls_of_term(pat.term))
     | Typ(typ) => Typ(ALFA_Typ.cls_of_term(typ.term))
     | TPat(tpat) => TPat(ALFA_TPat.cls_of_term(tpat.term));
diff --git a/src/haz3lcore/dynamics/Transition.re b/src/haz3lcore/dynamics/Transition.re
index 33ddc46ed..9a47d95ef 100644
--- a/src/haz3lcore/dynamics/Transition.re
+++ b/src/haz3lcore/dynamics/Transition.re
@@ -280,6 +280,8 @@ module Transition = (EV: EV_MODE) => {
         | Eval(e1, e2) => Eval(go_exp(e1), go_exp(e2))
         | Entail(ctx, p) => Entail(go_exp(ctx), go_exp(p))
         | Ctx(es) => Ctx(List.map(go_exp, es))
+        | Cons(e1, e2) => Cons(go_exp(e1), go_exp(e2))
+        | Concat(e1, e2) => Concat(go_exp(e1), go_exp(e2))
         | HasType(e, t) => HasType(go_exp(e), t)
         | Syn(e, t) => Syn(go_exp(e), t)
         | Ana(e, t) => Ana(go_exp(e), t)
@@ -309,8 +311,8 @@ module Transition = (EV: EV_MODE) => {
         | PrjR(e) => PrjR(go_exp(e))
         | InjL => InjL
         | InjR => InjR
-        | Case(e1, x, e2, y, e3) =>
-          Case(go_exp(e1), x, go_exp(e2), y, go_exp(e3))
+        | Case(e1, rls) =>
+          Case(go_exp(e1), List.map(((p, e)) => (p, go_exp(e)), rls))
         | Roll => Roll
         | Unroll => Unroll
         };
diff --git a/src/haz3lcore/lang/Form.re b/src/haz3lcore/lang/Form.re
index fef39cdee..5fa6b8527 100644
--- a/src/haz3lcore/lang/Form.re
+++ b/src/haz3lcore/lang/Form.re
@@ -400,14 +400,14 @@ let forms: list((string, t)) = [
   // Drv(Jdmt)
   ("fake_val", mk(ds, ["val", "end"], mk_op(Exp, [Exp]))),
   ("val", mk(ds, ["val", "end"], mk_op(Drv(Exp), [Drv(Exp)]))),
-  ("val_simple", mk(ii, [".val"], mk_post(P.min, Drv(Exp), []))),
-  ("fake_eval", mk(ds, ["eval", "to"], mk_pre(P.min, Exp, [Exp]))),
-  ("eval", mk(ds, ["eval", "to"], mk_pre(P.min, Drv(Exp), [Drv(Exp)]))),
-  ("eval_simple", mk_infix("$>", Drv(Exp), P.min)),
+  ("eval", mk_infix("\=/", Drv(Exp), P.min)),
   ("entail", mk_infix("|-", Drv(Exp), P.min)),
+  ("unary_entail", mk(ss, ["|-"], mk_pre(P.min, Drv(Exp), []))),
   // Drv(Ctx)
   ("alfa_exp_list", mk(ii, ["[", "]"], mk_op(Drv(Exp), [Drv(Exp)]))),
   ("alfa_cons", mk_infix(",", Drv(Exp), P.comma)),
+  ("alfa_concat", mk_infix("@", Drv(Exp), P.plus)),
+  ("alfa_cons", mk_infix("::", Drv(Exp), P.cons)),
   ("alfa_paren", mk(ii, ["(", ")"], mk_op(Drv(Exp), [Drv(Exp)]))),
   ("alfa_abbr", mk(ii, ["{", "}"], mk_op(Drv(Exp), [Pat]))),
   // Drv(Exp)
@@ -462,16 +462,13 @@ let forms: list((string, t)) = [
   ("exp_pair", mk_infix(",", Drv(Exp), P.comma)),
   ("exp_prjl", mk(ii, [".fst"], mk_post(P.ap, Drv(Exp), []))),
   ("exp_prjr", mk(ii, [".snd"], mk_post(P.ap, Drv(Exp), []))),
+  ("alfa_case", mk(ds, ["case", "end"], mk_op(Drv(Exp), [Drv(Rul)]))),
   (
-    "exp_case",
+    "alfa_rule",
     mk(
       ds,
-      ["case_sum", "of", "->", "else", "->"],
-      mk_pre(
-        P.fun_,
-        Drv(Exp),
-        [Drv(Exp), Drv(Pat), Drv(Exp), Drv(Pat)],
-      ),
+      ["|", "=>"],
+      mk_bin'(P.rule_sep, Drv(Rul), Drv(Exp), [Drv(Pat)], Drv(Exp)),
     ),
   ),
   // Drv(Pat)
diff --git a/src/haz3lcore/lang/Sort.re b/src/haz3lcore/lang/Sort.re
index c9df823fc..8afa6004f 100644
--- a/src/haz3lcore/lang/Sort.re
+++ b/src/haz3lcore/lang/Sort.re
@@ -5,6 +5,7 @@ module DrvSort = {
     | Ctx
     | Prop
     | Exp
+    | Rul
     | Pat
     | Typ
     | TPat;
@@ -15,6 +16,7 @@ module DrvSort = {
     | Prop => "Prop"
     | Ctx => "Ctx"
     | Exp => "ALFA_Exp"
+    | Rul => "ALFA_Rul"
     | Pat => "ALFA_Pat"
     | Typ => "ALFA_Typ"
     | TPat => "ALFA_TPat";
@@ -25,6 +27,7 @@ module DrvSort = {
     | Ctx => "Drv"
     | Prop => "Exp"
     | Exp => "Exp"
+    | Rul => "Rul"
     | Pat => "Pat"
     | Typ => "Typ"
     | TPat => "TPat";
@@ -37,6 +40,7 @@ module DrvSort = {
     | Ctx => "Ctx"
     | Prop => "Prop"
     | Exp => "ALFA_Exp"
+    | Rul => "ALFA_Rul"
     | Pat => "ALFA_Pat"
     | Typ => "ALFA_Typ"
     | TPat => "ALFA_TPat";
@@ -47,19 +51,21 @@ module DrvSort = {
     | Ctx => "context"
     | Prop => "proposition"
     | Exp => "ALFA expression"
+    | Rul => "ALFA rule"
     | Pat => "ALFA pattern"
     | Typ => "ALFA type"
     | TPat => "ALFA type pattern";
 
   let detail_sort: list(string) => t =
     fun
-    | [".val"] => Jdmt
     | ["val", "end"] => Jdmt
-    | ["eval", "to"] => Jdmt
     | ["|-"] => Jdmt
-    | ["$>"] => Jdmt
+    | ["\\=/"] => Jdmt
     | ["[]"] => Ctx
     | ["[", _] => Ctx
+    | [",", ",", _] => Ctx //TODO(zhiyao): not sufficient
+    | ["@"] => Ctx
+    | ["::"] => Ctx
     | _ => Exp;
 };
 
diff --git a/src/haz3lcore/lang/term/Drv.re b/src/haz3lcore/lang/term/Drv.re
index 94a406eed..616b05739 100644
--- a/src/haz3lcore/lang/term/Drv.re
+++ b/src/haz3lcore/lang/term/Drv.re
@@ -1,5 +1,6 @@
 include Term.Drv;
 module Exp = Term.ALFA_Exp;
+module Rul = Term.ALFA_Rul;
 module Pat = Term.ALFA_Pat;
 module Typ = Term.ALFA_Typ;
 module TPat = Term.ALFA_TPat;
diff --git a/src/haz3lcore/statics/MakeTerm.re b/src/haz3lcore/statics/MakeTerm.re
index 437703e51..d84882d2d 100644
--- a/src/haz3lcore/statics/MakeTerm.re
+++ b/src/haz3lcore/statics/MakeTerm.re
@@ -79,6 +79,27 @@ let is_rules = ((ts, kids): tiles): option(Aba.t(UPat.t, UExp.t)) => {
     |> OptUtil.sequence;
   Aba.mk(ps, clauses);
 };
+let is_alfa_rules =
+    ((ts, kids): tiles): option(Aba.t(Drv.Pat.t, Drv.Exp.t)) => {
+  open OptUtil.Syntax;
+  let+ ps =
+    ts
+    |> List.map(
+         fun
+         | (_, (["|", "=>"], [Any.Drv(Pat(p))])) => Some(p)
+         | _ => None,
+       )
+    |> OptUtil.sequence
+  and+ clauses =
+    kids
+    |> List.map(
+         fun
+         | Drv(Exp(clause)) => Some(clause)
+         | _ => None,
+       )
+    |> OptUtil.sequence;
+  Aba.mk(ps, clauses);
+};
 
 let ids_of_tiles = (tiles: tiles) => List.map(fst, Aba.get_as(tiles));
 let ids =
@@ -149,6 +170,7 @@ let rec go_s = (s: Sort.t, skel: Skel.t, seg: Segment.t): Term.Any.t =>
       | Ctx
       | Prop => failwith("unexpected drv sort")
       | Exp => Exp(alfa_exp(unsorted(skel, seg)))
+      | Rul => Rul(alfa_rul(unsorted(skel, seg)))
       | Pat => Pat(alfa_pat(unsorted(skel, seg)))
       | Typ => Typ(alfa_typ(unsorted(skel, seg)))
       | TPat => TPat(alfa_tpat(unsorted(skel, seg)))
@@ -212,12 +234,19 @@ and alfa_exp_term: unsorted => (Drv.Exp.term, list(Id.t)) = {
       }
     | (["(", ")"], [Drv(Exp(body))]) => ret(Parens(body))
     | (["{", "}"], [Pat(var)]) => ret(Abbr(var))
+    | (["case", "end"], [Drv(Rul({ids, term: Rules(scrut, rules), _}))]) => (
+        Case(scrut, rules),
+        ids,
+      )
     | _ => ret(hole(tm))
     }
   | Bin(Drv(Exp(l)), ([(_id, ([t], []))], []), Drv(Exp(r))) as tm =>
     switch (t) {
-    | "$>" => ret(Eval(l, r))
+    | "\\=/" => ret(Eval(l, r))
     | "|-" => ret(Entail(l, r))
+    | "," => ret(Tuple([l, r]))
+    | "::" => ret(Cons(l, r))
+    | "@" => ret(Concat(l, r))
     | "/\\" => ret(And(l, r))
     | "\\/" => ret(Or(l, r))
     | "==>" => ret(Impl(l, r))
@@ -227,7 +256,6 @@ and alfa_exp_term: unsorted => (Drv.Exp.term, list(Id.t)) = {
     | "==" => ret(Eq(l, r))
     | "<" => ret(Lt(l, r))
     | ">" => ret(Gt(l, r))
-    | "," => ret(Tuple([l, r]))
     | _ => ret(hole(tm))
     }
   | Bin(Drv(Exp(l)), tiles, Drv(Exp(r))) as tm =>
@@ -244,24 +272,18 @@ and alfa_exp_term: unsorted => (Drv.Exp.term, list(Id.t)) = {
     }
   | Pre(([(_id, t)], []), Drv(Exp(r))) as tm =>
     switch (t) {
-    | (["eval", "to"], [Drv(Exp(l))]) => ret(Eval(l, r))
     | (["-"], []) => ret(Neg(r))
+    | (["|-"], []) => ret(Entail(Ctx([]) |> Drv.Exp.fresh, r))
     | (["if", "then", "else"], [Drv(Exp(cond)), Drv(Exp(conseq))]) =>
       ret(If(cond, conseq, r))
     | (["let", "=", "in"], [Drv(Pat(pat)), Drv(Exp(def))]) =>
       ret(Let(pat, def, r))
     | (["fix", "->"], [Drv(Pat(pat))]) => ret(Fix(pat, r))
     | (["fun", "->"], [Drv(Pat(pat))]) => ret(Fun(pat, r))
-    | (
-        ["case_sum", "of", "->", "else", "->"],
-        [Drv(Exp(scrut)), Drv(Pat(pl)), Drv(Exp(l)), Drv(Pat(pr))],
-      ) =>
-      ret(Case(scrut, pl, l, pr, r))
     | _ => ret(hole(tm))
     }
   | Post(Drv(Exp(l)), ([(_id, t)], [])) as tm =>
     switch (t) {
-    | ([".val"], []) => ret(Val(l))
     | ([".fst"], []) => ret(PrjL(l))
     | ([".snd"], []) => ret(PrjR(l))
     | (["(", ")"], [Drv(Exp(r))]) => ret(Ap(l, r))
@@ -269,7 +291,26 @@ and alfa_exp_term: unsorted => (Drv.Exp.term, list(Id.t)) = {
     }
   | _ as tm => ret(hole(tm));
 }
-
+and alfa_rul = (unsorted: unsorted) => {
+  let hole = Drv.Rul.hole(kids_of_unsorted(unsorted));
+  switch (alfa_exp(unsorted)) {
+  | {term: Hole(MultiHole(_)), _} =>
+    switch (unsorted) {
+    | Bin(Drv(Exp(scrut)), tiles, Drv(Exp(last_clause))) =>
+      switch (is_alfa_rules(tiles)) {
+      | Some((ps, leading_clauses)) => {
+          ids: ids(unsorted),
+          term:
+            Rules(scrut, List.combine(ps, leading_clauses @ [last_clause])),
+          copied: false,
+        }
+      | None => {ids: ids(unsorted), term: hole, copied: false}
+      }
+    | _ => {ids: ids(unsorted), term: hole, copied: false}
+    }
+  | _ => {ids: ids(unsorted), term: hole, copied: false}
+  };
+}
 and alfa_pat = unsorted => {
   let (term, inner_ids) = alfa_pat_term(unsorted);
   let ids = ids(unsorted) @ inner_ids;
diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re
index 091615900..723059137 100644
--- a/src/haz3lcore/statics/Statics.re
+++ b/src/haz3lcore/statics/Statics.re
@@ -204,6 +204,10 @@ and drv_to_info_map =
     | Ctx(es) =>
       List.fold_left((m, e) => m |> go_exp(e, ~ty=Prop) |> snd, m, es)
       |> add'
+    | Cons(e1, e2) =>
+      m |> go_exp(e1, ~ty=Prop) |> snd |> go_exp(e2, ~ty=Ctx) |> snd |> add'
+    | Concat(e1, e2) =>
+      m |> go_exp(e1, ~ty=Ctx) |> snd |> go_exp(e2, ~ty=Ctx) |> snd |> add'
     | HasType(e, t)
     | Syn(e, t)
     | Ana(e, t) => m |> go_exp'(e) |> snd |> go_typ(t) |> snd |> add'
@@ -248,12 +252,13 @@ and drv_to_info_map =
     | InjR
     | Roll
     | Unroll => m |> add'
-    | Case(e, p1, e1, p2, e2) =>
+    | Case(e, [(p1, e1), (p2, e2)]) =>
       let m = m |> go_exp'(e) |> snd;
       let m = m |> go_pat(p1, ~expect=Ap_InjL) |> snd;
       let m = m |> go_exp'(e1) |> snd;
       let m = m |> go_pat(p2, ~expect=Ap_InjR) |> snd;
       m |> go_exp'(e2) |> snd |> add';
+    | Case(_) => m |> add'
     };
   }
   and go_exp' = go_exp(~ty=Exp)
@@ -309,6 +314,7 @@ and drv_to_info_map =
   };
   switch (drv) {
   | Exp(exp) => go_exp(exp, m, ~ty=Jdmt)
+  | Rul(_) => failwith("Statics.drv_to_info_map: impossible rul")
   | Pat(pat) => go_pat(pat, m, ~expect=Var)
   | Typ(ty) => go_typ(ty, m)
   | TPat(tp) => go_tpat(tp, m)
diff --git a/src/haz3lcore/statics/Term.re b/src/haz3lcore/statics/Term.re
index ea0a3840b..afcb3710d 100644
--- a/src/haz3lcore/statics/Term.re
+++ b/src/haz3lcore/statics/Term.re
@@ -625,6 +625,7 @@ module Any = {
   let rec ids =
     fun
     | Drv(Exp(tm)) => tm.ids
+    | Drv(Rul(tm)) => tm.ids
     | Drv(Pat(tm)) => tm.ids
     | Drv(Typ(tm)) => tm.ids
     | Drv(TPat(tm)) => tm.ids
@@ -650,6 +651,7 @@ module Any = {
   let rep_id =
     fun
     | Drv(Exp(tm)) => ALFA_Exp.rep_id(tm)
+    | Drv(Rul(tm)) => ALFA_Rul.rep_id(tm)
     | Drv(Pat(tm)) => ALFA_Pat.rep_id(tm)
     | Drv(Typ(tm)) => ALFA_Typ.rep_id(tm)
     | Drv(TPat(tm)) => ALFA_TPat.rep_id(tm)
diff --git a/src/haz3lcore/statics/TermBase.re b/src/haz3lcore/statics/TermBase.re
index 1a1280f11..1f9d45bf5 100644
--- a/src/haz3lcore/statics/TermBase.re
+++ b/src/haz3lcore/statics/TermBase.re
@@ -1247,12 +1247,14 @@ and Drv: {
   [@deriving (show({with_path: false}), sexp, yojson)]
   type t =
     | Exp(ALFA_Exp.t)
+    | Rul(ALFA_Rul.t)
     | Pat(ALFA_Pat.t)
     | Typ(ALFA_Typ.t)
     | TPat(ALFA_TPat.t);
 
   type mapper = {
     f_exp: (ALFA_Exp.t => ALFA_Exp.t, ALFA_Exp.t) => ALFA_Exp.t,
+    f_rul: (ALFA_Rul.t => ALFA_Rul.t, ALFA_Rul.t) => ALFA_Rul.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,
@@ -1267,12 +1269,14 @@ and Drv: {
   [@deriving (show({with_path: false}), sexp, yojson)]
   type t =
     | Exp(ALFA_Exp.t)
+    | Rul(ALFA_Rul.t)
     | Pat(ALFA_Pat.t)
     | Typ(ALFA_Typ.t)
     | TPat(ALFA_TPat.t);
 
   type mapper = {
     f_exp: (ALFA_Exp.t => ALFA_Exp.t, ALFA_Exp.t) => ALFA_Exp.t,
+    f_rul: (ALFA_Rul.t => ALFA_Rul.t, ALFA_Rul.t) => ALFA_Rul.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,
@@ -1280,18 +1284,31 @@ and Drv: {
 
   let drv_continue = {
     f_exp: continue,
+    f_rul: continue,
     f_pat: continue,
     f_typ: continue,
     f_tpat: continue,
   };
 
   let map_term = (~f_hazel_pat=continue, ~f_drv=drv_continue, x: t) => {
-    let {f_exp, f_pat, f_typ, f_tpat} = f_drv;
+    let {f_exp, f_rul, f_pat, f_typ, f_tpat} = f_drv;
     switch (x) {
     | Exp(exp) =>
       Exp(
         ALFA_Exp.map_term(~f_hazel_pat, ~f_exp, ~f_pat, ~f_typ, ~f_tpat, exp),
       )
+    | Rul(rul) =>
+      Rul(
+        ALFA_Rul.map_term(
+          ~f_hazel_pat,
+          ~f_exp,
+          ~f_rul,
+          ~f_pat,
+          ~f_typ,
+          ~f_tpat,
+          rul,
+        ),
+      )
     | Pat(pat) => Pat(ALFA_Pat.map_term(~f_pat, ~f_typ, ~f_tpat, pat))
     | Typ(typ) => Typ(ALFA_Typ.map_term(~f_typ, ~f_tpat, typ))
     | TPat(tpat) => TPat(ALFA_TPat.map_term(~f_tpat, tpat))
@@ -1302,6 +1319,8 @@ and Drv: {
     switch (x, y) {
     | (Exp(e1), Exp(e2)) => ALFA_Exp.fast_equal(e1, e2)
     | (Exp(_), _) => false
+    | (Rul(r1), Rul(r2)) => ALFA_Rul.fast_equal(r1, r2)
+    | (Rul(_), _) => false
     | (Pat(p1), Pat(p2)) => ALFA_Pat.fast_equal(p1, p2)
     | (Pat(_), _) => false
     | (Typ(t1), Typ(t2)) => ALFA_Typ.fast_equal(t1, t2)
@@ -1324,6 +1343,8 @@ and ALFA_Exp: {
     | Entail(t, t)
     // Ctx
     | Ctx(list(t))
+    | Cons(t, t)
+    | Concat(t, t)
     // Prop
     | HasType(t, ALFA_Typ.t)
     | Syn(t, ALFA_Typ.t)
@@ -1354,7 +1375,7 @@ and ALFA_Exp: {
     | PrjR(t)
     | InjL
     | InjR
-    | Case(t, ALFA_Pat.t, t, ALFA_Pat.t, t)
+    | Case(t, list((ALFA_Pat.t, t)))
     | Roll
     | Unroll
   and t = IdTagged.t(term);
@@ -1385,6 +1406,8 @@ and ALFA_Exp: {
     | Entail(t, t)
     // Ctx
     | Ctx(list(t))
+    | Cons(t, t)
+    | Concat(t, t)
     // Prop
     | HasType(t, ALFA_Typ.t)
     | Syn(t, ALFA_Typ.t)
@@ -1415,7 +1438,7 @@ and ALFA_Exp: {
     | PrjR(t)
     | InjL
     | InjR
-    | Case(t, ALFA_Pat.t, t, ALFA_Pat.t, t)
+    | Case(t, list((ALFA_Pat.t, t)))
     | Roll
     | Unroll
   and t = IdTagged.t(term);
@@ -1444,6 +1467,8 @@ and ALFA_Exp: {
         | Eval(e1, e2) => Eval(exp_map_term(e1), exp_map_term(e2))
         | Entail(e1, e2) => Entail(exp_map_term(e1), exp_map_term(e2))
         | Ctx(e) => Ctx(List.map(exp_map_term, e))
+        | Cons(e1, e2) => Cons(exp_map_term(e1), exp_map_term(e2))
+        | Concat(e1, e2) => Concat(exp_map_term(e1), exp_map_term(e2))
         | HasType(e, t) => HasType(exp_map_term(e), t)
         | Syn(e, t) => Syn(exp_map_term(e), t)
         | Ana(e, t) => Ana(exp_map_term(e), t)
@@ -1475,13 +1500,13 @@ and ALFA_Exp: {
         | PrjR(e) => PrjR(exp_map_term(e))
         | InjL => InjL
         | InjR => InjR
-        | Case(e, p1, e1, p2, e2) =>
+        | Case(e, rls) =>
           Case(
             exp_map_term(e),
-            pat_map_term(p1),
-            exp_map_term(e1),
-            pat_map_term(p2),
-            exp_map_term(e2),
+            List.map(
+              ((p, e)) => (pat_map_term(p), exp_map_term(e)),
+              rls,
+            ),
           )
         | Roll => Roll
         | Unroll => Unroll
@@ -1511,6 +1536,12 @@ and ALFA_Exp: {
       List.length(es1) == List.length(es2)
       && List.for_all2(ALFA_Exp.fast_equal, es1, es2)
     | (Ctx(_), _) => false
+    | (Cons(e11, e12), Cons(e21, e22)) =>
+      ALFA_Exp.fast_equal(e11, e21) && ALFA_Exp.fast_equal(e12, e22)
+    | (Cons(_), _) => false
+    | (Concat(e11, e12), Concat(e21, e22)) =>
+      ALFA_Exp.fast_equal(e11, e21) && ALFA_Exp.fast_equal(e12, e22)
+    | (Concat(_), _) => false
     | (HasType(e1, t1), HasType(e2, t2)) =>
       ALFA_Exp.fast_equal(e1, e2) && ALFA_Typ.fast_equal(t1, t2)
     | (HasType(_), _) => false
@@ -1592,12 +1623,15 @@ and ALFA_Exp: {
     | (InjL, _) => false
     | (InjR, InjR) => true
     | (InjR, _) => false
-    | (Case(e1, p1, e11, p2, e12), Case(e2, p3, e21, p4, e22)) =>
+    | (Case(e1, rls1), Case(e2, rls2)) =>
       ALFA_Exp.fast_equal(e1, e2)
-      && ALFA_Pat.fast_equal(p1, p3)
-      && ALFA_Exp.fast_equal(e11, e21)
-      && ALFA_Pat.fast_equal(p2, p4)
-      && ALFA_Exp.fast_equal(e12, e22)
+      && List.length(rls1) == List.length(rls2)
+      && List.for_all2(
+           ((p1, e1), (p2, e2)) =>
+             ALFA_Pat.fast_equal(p1, p2) && ALFA_Exp.fast_equal(e1, e2),
+           rls1,
+           rls2,
+         )
     | (Case(_), _) => false
     | (Roll, Roll) => true
     | (Roll, _) => false
@@ -1605,6 +1639,79 @@ and ALFA_Exp: {
     | (Unroll, _) => false
     };
 }
+and ALFA_Rul: {
+  [@deriving (show({with_path: false}), sexp, yojson)]
+  type term =
+    | Hole(TypeHole.t)
+    | Rules(ALFA_Exp.t, list((ALFA_Pat.t, ALFA_Exp.t)))
+  and t = IdTagged.t(term);
+
+  let map_term:
+    (
+      ~f_hazel_pat: Pat.t => Pat.t=?,
+      ~f_exp: (ALFA_Exp.t => ALFA_Exp.t, ALFA_Exp.t) => ALFA_Exp.t=?,
+      ~f_rul: (ALFA_Rul.t => ALFA_Rul.t, ALFA_Rul.t) => ALFA_Rul.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)
+    | Rules(ALFA_Exp.t, list((ALFA_Pat.t, ALFA_Exp.t)))
+  and t = IdTagged.t(term);
+
+  let map_term =
+      (
+        ~f_hazel_pat=continue,
+        ~f_exp=continue,
+        ~f_rul=continue,
+        ~f_pat=continue,
+        ~f_typ=continue,
+        ~f_tpat=continue,
+        x,
+      ) => {
+    let exp_map_term =
+      ALFA_Exp.map_term(~f_hazel_pat, ~f_exp, ~f_pat, ~f_typ, ~f_tpat);
+    let pat_map_term = ALFA_Pat.map_term(~f_pat, ~f_typ, ~f_tpat);
+    let rec_call = ({term, _} as exp: t) => {
+      ...exp,
+      term:
+        switch (term) {
+        | Hole(_) => term
+        | Rules(e, rls) =>
+          Rules(
+            exp_map_term(e),
+            List.map(
+              ((p, e)) => (pat_map_term(p), exp_map_term(e)),
+              rls,
+            ),
+          )
+        },
+    };
+    x |> f_rul(rec_call);
+  };
+
+  let fast_equal = (r1: t, r2: t) =>
+    switch (r1 |> IdTagged.term_of, r2 |> IdTagged.term_of) {
+    | (Hole(_), _) => false
+    | (Rules(e1, rls1), Rules(e2, rls2)) =>
+      ALFA_Exp.fast_equal(e1, e2)
+      && List.length(rls1) == List.length(rls2)
+      && List.for_all2(
+           ((p1, e1), (p2, e2)) =>
+             ALFA_Pat.fast_equal(p1, p2) && ALFA_Exp.fast_equal(e1, e2),
+           rls1,
+           rls2,
+         )
+    | (Rules(_), _) => false
+    };
+}
 and ALFA_Pat: {
   [@deriving (show({with_path: false}), sexp, yojson)]
   type term =
diff --git a/src/haz3lcore/tiles/Segment.re b/src/haz3lcore/tiles/Segment.re
index 82aad0424..75a158f96 100644
--- a/src/haz3lcore/tiles/Segment.re
+++ b/src/haz3lcore/tiles/Segment.re
@@ -126,7 +126,8 @@ and subsort_of = (sort: Sort.t): list(Sort.t) =>
       | Jdmt
       | Ctx
       | Prop => failwith("subsort_of unexpected")
-      | Exp => [Pat, Typ, TPat]
+      | Exp => [Rul, Pat, Typ, TPat]
+      | Rul => [Exp, Pat, Typ, TPat]
       | Pat => [Typ]
       | Typ => []
       | TPat => [Typ]
diff --git a/src/haz3lcore/zipper/action/Insert.re b/src/haz3lcore/zipper/action/Insert.re
index a59de12f8..f0ef0e294 100644
--- a/src/haz3lcore/zipper/action/Insert.re
+++ b/src/haz3lcore/zipper/action/Insert.re
@@ -192,7 +192,6 @@ let go =
     : 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