diff --git a/src/haz3lcore/dynamics/DH.re b/src/haz3lcore/dynamics/DH.re
index 591dfd6013..0e4e0ef0ad 100644
--- a/src/haz3lcore/dynamics/DH.re
+++ b/src/haz3lcore/dynamics/DH.re
@@ -22,6 +22,7 @@ module rec DHExp: {
     | FixF(Var.t, Typ.t, t)
     | Fun(DHPat.t, Typ.t, t, option(Var.t))
     | Ap(t, t)
+    | Derive(t, t, t)
     | ApBuiltin(string, t)
     | BuiltinFun(string)
     | Test(KeywordID.t, t)
@@ -84,6 +85,7 @@ module rec DHExp: {
     | FixF(Var.t, Typ.t, t)
     | Fun(DHPat.t, Typ.t, t, option(Var.t))
     | Ap(t, t)
+    | Derive(t, t, t)
     | ApBuiltin(string, t)
     | BuiltinFun(string)
     | Test(KeywordID.t, t)
@@ -131,6 +133,7 @@ module rec DHExp: {
     | Fun(_, _, _, _) => "Fun"
     | Closure(_, _) => "Closure"
     | Ap(_, _) => "Ap"
+    | Derive(_, _, _) => "Derive"
     | ApBuiltin(_, _) => "ApBuiltin"
     | BuiltinFun(_) => "BuiltinFun"
     | Test(_) => "Test"
@@ -195,6 +198,8 @@ module rec DHExp: {
     | FixF(a, b, c) => FixF(a, b, strip_casts(c))
     | Fun(a, b, c, d) => Fun(a, b, strip_casts(c), d)
     | Ap(a, b) => Ap(strip_casts(a), strip_casts(b))
+    | Derive(a, b, c) =>
+      Derive(strip_casts(a), strip_casts(b), strip_casts(c))
     | Test(id, a) => Test(id, strip_casts(a))
     | ApBuiltin(fn, args) => ApBuiltin(fn, strip_casts(args))
     | BuiltinFun(fn) => BuiltinFun(fn)
@@ -265,7 +270,10 @@ module rec DHExp: {
       f1 == f2 && ty1 == ty2 && fast_equal(d1, d2)
     | (Fun(dp1, ty1, d1, s1), Fun(dp2, ty2, d2, s2)) =>
       dp1 == dp2 && ty1 == ty2 && fast_equal(d1, d2) && s1 == s2
-    | (Ap(d11, d21), Ap(d12, d22))
+    | (Ap(d11, d21), Ap(d12, d22)) =>
+      fast_equal(d11, d12) && fast_equal(d21, d22)
+    | (Derive(d11, d21, d31), Derive(d12, d22, d32)) =>
+      fast_equal(d11, d12) && fast_equal(d21, d22) && fast_equal(d31, d32)
     | (Cons(d11, d21), Cons(d12, d22)) =>
       fast_equal(d11, d12) && fast_equal(d21, d22)
     | (ListConcat(d11, d21), ListConcat(d12, d22)) =>
@@ -314,6 +322,7 @@ module rec DHExp: {
     | (Fun(_), _)
     | (Test(_), _)
     | (Ap(_), _)
+    | (Derive(_), _)
     | (ApBuiltin(_), _)
     | (BuiltinFun(_), _)
     | (Cons(_), _)
diff --git a/src/haz3lcore/dynamics/Elaborator.re b/src/haz3lcore/dynamics/Elaborator.re
index 0141cf18a9..65e3dde5d5 100644
--- a/src/haz3lcore/dynamics/Elaborator.re
+++ b/src/haz3lcore/dynamics/Elaborator.re
@@ -92,6 +92,7 @@ let cast = (ctx: Ctx.t, mode: Mode.t, self_ty: Typ.t, d: DHExp.t) =>
     /* Normal cases: wrap */
     | BoundVar(_)
     | Ap(_)
+    | Derive(_)
     | ApBuiltin(_)
     | BuiltinFun(_)
     | Prj(_)
@@ -285,6 +286,11 @@ let rec dhexp_of_uexp =
         let* c_fn = dhexp_of_uexp(m, fn);
         let+ c_arg = dhexp_of_uexp(m, arg);
         DHExp.Ap(c_fn, c_arg);
+      | Derive(conclusion, premises, rule) =>
+        let* dconcl = dhexp_of_uexp(m, conclusion);
+        let* dprems = dhexp_of_uexp(m, premises);
+        let+ drule = dhexp_of_uexp(m, rule);
+        DHExp.Derive(dconcl, dprems, drule);
       | DeferredAp(fn, args) =>
         switch (err_status) {
         | InHole(BadPartialAp(NoDeferredArgs)) => dhexp_of_uexp(m, fn)
diff --git a/src/haz3lcore/dynamics/EvalCtx.re b/src/haz3lcore/dynamics/EvalCtx.re
index 2ca2fbaadc..3d2d026759 100644
--- a/src/haz3lcore/dynamics/EvalCtx.re
+++ b/src/haz3lcore/dynamics/EvalCtx.re
@@ -13,6 +13,9 @@ type cls =
   | Let2
   | Ap1
   | Ap2
+  | Derive1
+  | Derive2
+  | Derive3
   | Fun
   | FixF
   | BinBoolOp1
@@ -65,6 +68,9 @@ type t =
   | FixF(Var.t, Typ.t, t)
   | Ap1(t, DHExp.t)
   | Ap2(DHExp.t, t)
+  | Derive1(t, DHExp.t, DHExp.t)
+  | Derive2(DHExp.t, t, DHExp.t)
+  | Derive3(DHExp.t, DHExp.t, t)
   | IfThenElse1(if_consistency, t, DHExp.t, DHExp.t)
   | IfThenElse2(if_consistency, DHExp.t, t, DHExp.t)
   | IfThenElse3(if_consistency, DHExp.t, DHExp.t, t)
@@ -138,6 +144,9 @@ let rec fuzzy_mark =
   | FixF(_)
   | Ap1(_)
   | Ap2(_)
+  | Derive1(_)
+  | Derive2(_)
+  | Derive3(_)
   | IfThenElse1(_)
   | IfThenElse2(_)
   | IfThenElse3(_)
diff --git a/src/haz3lcore/dynamics/EvaluatorPost.re b/src/haz3lcore/dynamics/EvaluatorPost.re
index 76e0d2a9ab..8e801c5dfd 100644
--- a/src/haz3lcore/dynamics/EvaluatorPost.re
+++ b/src/haz3lcore/dynamics/EvaluatorPost.re
@@ -64,6 +64,12 @@ let rec pp_eval = (d: DHExp.t): m(DHExp.t) =>
     let* d2' = pp_eval(d2);
     Ap(d1', d2') |> return;
 
+  | Derive(d1, d2, d3) =>
+    let* d1' = pp_eval(d1);
+    let* d2' = pp_eval(d2);
+    let+ d3' = pp_eval(d3);
+    Derive(d1', d2', d3');
+
   | ApBuiltin(f, d1) =>
     let* d1' = pp_eval(d1);
     ApBuiltin(f, d1') |> return;
@@ -321,6 +327,12 @@ and pp_uneval = (env: ClosureEnvironment.t, d: DHExp.t): m(DHExp.t) =>
     let* d2' = pp_uneval(env, d2);
     Ap(d1', d2') |> return;
 
+  | Derive(d1, d2, d3) =>
+    let* d1' = pp_uneval(env, d1);
+    let* d2' = pp_uneval(env, d2);
+    let+ d3' = pp_uneval(env, d3);
+    Derive(d1', d2', d3');
+
   | ApBuiltin(f, d1) =>
     let* d1' = pp_uneval(env, d1);
     ApBuiltin(f, d1') |> return;
@@ -545,6 +557,11 @@ let rec track_children_of_hole =
       track_children_of_hole_rules(hii, parent, rules)
     );
 
+  | Derive(d1, d2, d3) =>
+    let hii = track_children_of_hole(hii, parent, d1);
+    let hii = track_children_of_hole(hii, parent, d2);
+    track_children_of_hole(hii, parent, d3);
+
   | ApBuiltin(_, d) => track_children_of_hole(hii, parent, d)
 
   /* Hole types */
diff --git a/src/haz3lcore/dynamics/EvaluatorStep.re b/src/haz3lcore/dynamics/EvaluatorStep.re
index c92d3f0953..282bca96d7 100644
--- a/src/haz3lcore/dynamics/EvaluatorStep.re
+++ b/src/haz3lcore/dynamics/EvaluatorStep.re
@@ -234,6 +234,15 @@ let rec compose = (ctx: EvalCtx.t, d: DHExp.t): DHExp.t => {
     | Ap2(d1, ctx) =>
       let d2 = compose(ctx, d);
       Ap(d1, d2);
+    | Derive1(ctx, d2, d3) =>
+      let d1 = compose(ctx, d);
+      Derive(d1, d2, d3);
+    | Derive2(d1, ctx, d3) =>
+      let d2 = compose(ctx, d);
+      Derive(d1, d2, d3);
+    | Derive3(d1, d2, ctx) =>
+      let d3 = compose(ctx, d);
+      Derive(d1, d2, d3);
     | ApBuiltin(s, ctx) =>
       let d' = compose(ctx, d);
       ApBuiltin(s, d');
diff --git a/src/haz3lcore/dynamics/FilterMatcher.re b/src/haz3lcore/dynamics/FilterMatcher.re
index 17b8472a86..6431e613b1 100644
--- a/src/haz3lcore/dynamics/FilterMatcher.re
+++ b/src/haz3lcore/dynamics/FilterMatcher.re
@@ -109,6 +109,12 @@ let rec matches_exp =
     matches_exp(env, d1, f1) && matches_exp(env, d2, f2)
   | (Ap(_), _) => false
 
+  | (Derive(d1, d2, d3), Derive(f1, f2, f3)) =>
+    matches_exp(env, d1, f1)
+    && matches_exp(env, d2, f2)
+    && matches_exp(env, d3, f3)
+  | (Derive(_), _) => false
+
   | (IfThenElse(dc, d1, d2, d3), IfThenElse(fc, f1, f2, f3)) =>
     dc == fc
     && matches_exp(env, d1, f1)
diff --git a/src/haz3lcore/dynamics/PatternMatch.re b/src/haz3lcore/dynamics/PatternMatch.re
index 16145e995f..57ca4f19d7 100644
--- a/src/haz3lcore/dynamics/PatternMatch.re
+++ b/src/haz3lcore/dynamics/PatternMatch.re
@@ -241,6 +241,7 @@ and matches_cast_Sum =
   | InvalidText(_)
   | Let(_)
   | Ap(_)
+  | Derive(_)
   | ApBuiltin(_)
   | BinBoolOp(_)
   | BinIntOp(_)
@@ -344,6 +345,7 @@ and matches_cast_Tuple =
   | Closure(_, _) => IndetMatch
   | Filter(_, _) => IndetMatch
   | Ap(_, _) => IndetMatch
+  | Derive(_) => IndetMatch
   | ApBuiltin(_, _) => IndetMatch
   | BinBoolOp(_, _, _)
   | BinIntOp(_, _, _)
@@ -488,6 +490,7 @@ and matches_cast_Cons =
   | Closure(_, d') => matches_cast_Cons(dp, d', elt_casts)
   | Filter(_, d') => matches_cast_Cons(dp, d', elt_casts)
   | Ap(_, _) => IndetMatch
+  | Derive(_) => IndetMatch
   | ApBuiltin(_, _) => IndetMatch
   | BinBoolOp(_, _, _)
   | BinIntOp(_, _, _)
diff --git a/src/haz3lcore/dynamics/Stepper.re b/src/haz3lcore/dynamics/Stepper.re
index d75b023ab8..e68f58c773 100644
--- a/src/haz3lcore/dynamics/Stepper.re
+++ b/src/haz3lcore/dynamics/Stepper.re
@@ -89,6 +89,15 @@ let rec matches =
     | Ap2(d1, ctx) =>
       let+ ctx = matches(env, flt, ctx, exp, act, idx);
       Ap2(d1, ctx);
+    | Derive1(ctx, d2, d3) =>
+      let+ ctx = matches(env, flt, ctx, exp, act, idx);
+      Derive1(ctx, d2, d3);
+    | Derive2(d1, ctx, d3) =>
+      let+ ctx = matches(env, flt, ctx, exp, act, idx);
+      Derive2(d1, ctx, d3);
+    | Derive3(d1, d2, ctx) =>
+      let+ ctx = matches(env, flt, ctx, exp, act, idx);
+      Derive3(d1, d2, ctx);
     | IfThenElse1(c, ctx, d2, d3) =>
       let+ ctx = matches(env, flt, ctx, exp, act, idx);
       IfThenElse1(c, ctx, d2, d3);
diff --git a/src/haz3lcore/dynamics/Substitution.re b/src/haz3lcore/dynamics/Substitution.re
index 2b2da68c3a..1a1343b161 100644
--- a/src/haz3lcore/dynamics/Substitution.re
+++ b/src/haz3lcore/dynamics/Substitution.re
@@ -52,6 +52,11 @@ let rec subst_var = (d1: DHExp.t, x: Var.t, d2: DHExp.t): DHExp.t =>
     let d3 = subst_var(d1, x, d3);
     let d4 = subst_var(d1, x, d4);
     Ap(d3, d4);
+  | Derive(d3, d4, d5) =>
+    let d3 = subst_var(d1, x, d3);
+    let d4 = subst_var(d1, x, d4);
+    let d5 = subst_var(d1, x, d5);
+    Derive(d3, d4, d5);
   | ApBuiltin(ident, d1) =>
     let d2 = subst_var(d1, x, d1);
     ApBuiltin(ident, d2);
diff --git a/src/haz3lcore/dynamics/Transition.re b/src/haz3lcore/dynamics/Transition.re
index 63a02b2d26..722fd84456 100644
--- a/src/haz3lcore/dynamics/Transition.re
+++ b/src/haz3lcore/dynamics/Transition.re
@@ -305,6 +305,47 @@ module Transition = (EV: EV_MODE) => {
           value: true,
         })
       };
+    | Derive(conclusion, premises, rule) =>
+      let. _ =
+        otherwise(env, (conclusion, premises, rule) =>
+          Derive(conclusion, premises, rule)
+        )
+      and. rule' =
+        req_final(
+          req(state, env),
+          rule => Derive3(conclusion, premises, rule),
+          rule,
+        )
+      and. premises' =
+        req_final(
+          req(state, env),
+          premises => Derive2(conclusion, premises, rule),
+          premises,
+        )
+      and. conclusion' =
+        req_final(
+          req(state, env),
+          conclusion => Derive1(conclusion, premises, rule),
+          conclusion,
+        );
+      switch (rule') {
+      | BuiltinFun(ident) =>
+        Step({
+          apply: () => {
+            ApBuiltin(ident, Tuple([conclusion', premises']));
+          },
+          kind: BuiltinAp(ident),
+          value: false,
+        })
+      | _ =>
+        Step({
+          apply: () => {
+            raise(EvaluatorError.Exception(InvalidBoxedFun(rule')));
+          },
+          kind: InvalidStep,
+          value: true,
+        })
+      };
     | ApBuiltin(ident, arg) =>
       let. _ = otherwise(env, arg => ApBuiltin(ident, arg))
       and. arg' =
diff --git a/src/haz3lcore/statics/MakeTerm.re b/src/haz3lcore/statics/MakeTerm.re
index e454e0f2ac..3c805c6dae 100644
--- a/src/haz3lcore/statics/MakeTerm.re
+++ b/src/haz3lcore/statics/MakeTerm.re
@@ -186,6 +186,8 @@ and exp_term: unsorted => (UExp.term, list(Id.t)) = {
         | (["!"], []) => UnOp(Bool(Not), r)
         | (["fun", "->"], [Pat(pat)]) => Fun(pat, r)
         | (["let", "=", "in"], [Pat(pat), Exp(def)]) => Let(pat, def, r)
+        | (["der", "\\", "of"], [Exp(conclusion), Exp(premises)]) =>
+          Derive(conclusion, premises, r)
         | (["hide", "in"], [Exp(filter)]) =>
           Filter((Eval, One), filter, r)
         | (["eval", "in"], [Exp(filter)]) =>
diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re
index 3357808835..38bbb9e003 100644
--- a/src/haz3lcore/statics/Statics.re
+++ b/src/haz3lcore/statics/Statics.re
@@ -330,6 +330,20 @@ and uexp_to_info_map =
       && !Typ.is_consistent(ctx, ty_in, Prod([]))
         ? BadTrivAp(ty_in) : Just(ty_out);
     add(~self, ~co_ctx=CoCtx.union([fn.co_ctx, arg.co_ctx]), m);
+  | Derive(conclusion, premises, rule) =>
+    let (rule, m) =
+      go(
+        ~mode=Ana(Arrow(Prod([Judgement, List(Judgement)]), Judgement)),
+        rule,
+        m,
+      );
+    let (conclusion, m) = go(~mode=Ana(Judgement), conclusion, m);
+    let (premises, m) = go(~mode=Ana(List(Judgement)), premises, m);
+    add(
+      ~self=Just(Judgement),
+      ~co_ctx=CoCtx.union([rule.co_ctx, conclusion.co_ctx, premises.co_ctx]),
+      m,
+    );
   | DeferredAp(fn, args) =>
     let fn_mode = Mode.of_ap(ctx, mode, UExp.ctr_name(fn));
     let (fn, m) = go(~mode=fn_mode, fn, m);
diff --git a/src/haz3lcore/statics/Term.re b/src/haz3lcore/statics/Term.re
index 7522c92859..503d2d9c0b 100644
--- a/src/haz3lcore/statics/Term.re
+++ b/src/haz3lcore/statics/Term.re
@@ -404,6 +404,7 @@ module UExp = {
     | Let
     | TyAlias
     | Ap
+    | Derive
     | DeferredAp
     | Pipeline
     | If
@@ -451,6 +452,7 @@ module UExp = {
     | Let(_) => Let
     | TyAlias(_) => TyAlias
     | Ap(_) => Ap
+    | Derive(_) => Derive
     | DeferredAp(_) => DeferredAp
     | Pipeline(_) => Pipeline
     | If(_) => If
@@ -557,6 +559,7 @@ module UExp = {
     | Let => "Let expression"
     | TyAlias => "Type Alias definition"
     | Ap => "Application"
+    | Derive => "Derivation"
     | DeferredAp => "Partial Application"
     | Pipeline => "Pipeline expression"
     | If => "If expression"
@@ -592,6 +595,7 @@ module UExp = {
     | Let(_)
     | TyAlias(_)
     | Ap(_)
+    | Derive(_)
     | DeferredAp(_)
     | Pipeline(_)
     | If(_)
@@ -631,6 +635,7 @@ module UExp = {
       | Let(_)
       | TyAlias(_)
       | Ap(_)
+      | Derive(_)
       | DeferredAp(_)
       | Pipeline(_)
       | If(_)
@@ -685,6 +690,7 @@ module UExp = {
       | Filter(_)
       | TyAlias(_)
       | Ap(_)
+      | Derive(_)
       | DeferredAp(_)
       | Pipeline(_)
       | If(_)
diff --git a/src/haz3lcore/statics/TermBase.re b/src/haz3lcore/statics/TermBase.re
index c4cfaf3bb0..2c2d4f6041 100644
--- a/src/haz3lcore/statics/TermBase.re
+++ b/src/haz3lcore/statics/TermBase.re
@@ -128,6 +128,7 @@ and UExp: {
     | Var
     | Let
     | Ap
+    | Derive
     | If
     | Seq
     | Test
@@ -166,6 +167,7 @@ and UExp: {
     | Let(UPat.t, t, t)
     | TyAlias(UTPat.t, UTyp.t, t)
     | Ap(t, t)
+    | Derive(t, t, t)
     | DeferredAp(t, list(t))
     | Pipeline(t, t)
     | If(t, t, t)
@@ -280,6 +282,7 @@ and UExp: {
     | Var
     | Let
     | Ap
+    | Derive
     | If
     | Seq
     | Test
@@ -318,6 +321,7 @@ and UExp: {
     | Let(UPat.t, t, t)
     | TyAlias(UTPat.t, UTyp.t, t)
     | Ap(t, t)
+    | Derive(t, t, t)
     | DeferredAp(t, list(t))
     | Pipeline(t, t)
     | If(t, t, t)
diff --git a/src/haz3lcore/zipper/EditorUtil.re b/src/haz3lcore/zipper/EditorUtil.re
index c8d58cd794..c593a0eefa 100644
--- a/src/haz3lcore/zipper/EditorUtil.re
+++ b/src/haz3lcore/zipper/EditorUtil.re
@@ -60,6 +60,7 @@ let rec append_exp = (e1: TermBase.UExp.t, e2: TermBase.UExp.t) => {
   | Tuple(_)
   | Var(_)
   | Ap(_)
+  | Derive(_)
   | DeferredAp(_)
   | Pipeline(_)
   | If(_)
diff --git a/src/haz3lschool/SyntaxTest.re b/src/haz3lschool/SyntaxTest.re
index 756fa6a268..bef09d0a5b 100644
--- a/src/haz3lschool/SyntaxTest.re
+++ b/src/haz3lschool/SyntaxTest.re
@@ -86,6 +86,7 @@ let rec find_fn =
   | ListConcat(u1, u2)
   | Entail(u1, u2)
   | BinOp(_, u1, u2) => l |> find_fn(name, u1) |> find_fn(name, u2)
+  | Derive(u1, u2, u3)
   | If(u1, u2, u3) =>
     l |> find_fn(name, u1) |> find_fn(name, u2) |> find_fn(name, u3)
   | DeferredAp(fn, args) =>
@@ -186,6 +187,7 @@ let rec var_mention = (name: string, uexp: Term.UExp.t): bool => {
   | BinOp(_, u1, u2) => var_mention(name, u1) || var_mention(name, u2)
   | DeferredAp(u1, us) =>
     var_mention(name, u1) || List.exists(var_mention(name), us)
+  | Derive(u1, u2, u3)
   | If(u1, u2, u3) =>
     var_mention(name, u1) || var_mention(name, u2) || var_mention(name, u3)
   | Match(g, l) =>
@@ -238,6 +240,10 @@ let rec var_applied = (name: string, uexp: Term.UExp.t): bool => {
     | Var(x) => x == name ? true : var_applied(name, u2)
     | _ => var_applied(name, u1) || var_applied(name, u2)
     }
+  | Derive(concl, prems, rule) =>
+    var_applied(name, concl)
+    || var_applied(name, prems)
+    || var_applied(name, rule)
   | DeferredAp(u1, us) =>
     switch (u1.term) {
     | Var(x) => x == name ? true : List.exists(var_applied(name), us)
@@ -319,6 +325,10 @@ let rec tail_check = (name: string, uexp: Term.UExp.t): bool => {
   | Parens(u) => tail_check(name, u)
   | UnOp(_, u) => !var_mention(name, u)
   | Ap(u1, u2) => var_mention(name, u2) ? false : tail_check(name, u1)
+  | Derive(concl, prems, rule) =>
+    var_mention(name, concl)
+    || var_mention(name, prems)
+    || var_mention(name, rule)
   | DeferredAp(fn, args) =>
     tail_check(
       name,
diff --git a/src/haz3lweb/explainthis/Example.re b/src/haz3lweb/explainthis/Example.re
index 74ca7a6d8a..7e3091b70d 100644
--- a/src/haz3lweb/explainthis/Example.re
+++ b/src/haz3lweb/explainthis/Example.re
@@ -120,6 +120,7 @@ let typeann = () => mk_monotile(Form.get("typeann"));
 let mk_fun = mk_tile(Form.get("fun_"));
 let mk_ap_exp = mk_tile(Form.get("ap_exp"));
 let mk_ap_pat = mk_tile(Form.get("ap_pat"));
+let mk_derive = mk_tile(Form.get("derive"));
 let mk_let = mk_tile(Form.get("let_"));
 let mk_tyalias = mk_tile(Form.get("type_alias"));
 let mk_if = mk_tile(Form.get("if_"));
diff --git a/src/haz3lweb/explainthis/ExplainThisForm.re b/src/haz3lweb/explainthis/ExplainThisForm.re
index 6e827bddbc..7dc664b370 100644
--- a/src/haz3lweb/explainthis/ExplainThisForm.re
+++ b/src/haz3lweb/explainthis/ExplainThisForm.re
@@ -80,6 +80,7 @@ type example_id =
   | Let(let_examples)
   | FunAp
   | ConAp
+  | Derive
   | DeferredAp
   | IfTrue
   | IfFalse
@@ -160,6 +161,7 @@ type form_id =
   | LetExp(pat_sub_form_id)
   | FunApExp
   | ConApExp
+  | DeriveExp
   | DeferredApExp
   | IfExp
   | SeqExp
@@ -252,6 +254,7 @@ type group_id =
   | LetExp(pat_sub_form_id)
   | FunApExp
   | ConApExp
+  | DeriveExp
   | DeferredApExp
   | IfExp
   | SeqExp
diff --git a/src/haz3lweb/explainthis/data/DeriveExp.re b/src/haz3lweb/explainthis/data/DeriveExp.re
new file mode 100644
index 0000000000..28656f9def
--- /dev/null
+++ b/src/haz3lweb/explainthis/data/DeriveExp.re
@@ -0,0 +1,39 @@
+open Haz3lcore;
+open ExplainThisForm;
+open Example;
+
+let if_basic1_exp_ex = {
+  sub_id: Derive,
+  term: mk_example("der []|-truth \\ [] of rule_Truth_I"),
+  message: "The truth rule states that ⊤ is true.",
+};
+
+let _exp_concl = exp("e_concl");
+let _exp_rule = exp("e_rule");
+let _exp_prem = exp("e_prem");
+let derive_exp_coloring_ids =
+    (~concl_id: Id.t, ~prems_id: Id.t, ~rule_id: Id.t): list((Id.t, Id.t)) => [
+  (Piece.id(_exp_concl), concl_id),
+  (Piece.id(_exp_rule), rule_id),
+  (Piece.id(_exp_prem), prems_id),
+];
+
+let derive_exp: form = {
+  let explanation = "To derive the [*conclusion*](%s), use the [*rule*](%s) with the [*premises*](%s).";
+  {
+    id: DeriveExp,
+    syntactic_form: [
+      mk_derive([
+        [space(), _exp_concl, linebreak()],
+        [space(), _exp_rule, linebreak()],
+      ]),
+      space(),
+      _exp_prem,
+    ],
+    expandable_id: None,
+    explanation,
+    examples: [if_basic1_exp_ex],
+  };
+};
+
+let derives: group = {id: DeriveExp, forms: [derive_exp]};
diff --git a/src/haz3lweb/view/ExplainThis.re b/src/haz3lweb/view/ExplainThis.re
index cc373c3438..d4679be424 100644
--- a/src/haz3lweb/view/ExplainThis.re
+++ b/src/haz3lweb/view/ExplainThis.re
@@ -1609,6 +1609,26 @@ let get_doc =
           let color_map = (mapping, List.length(args) + 1);
           ([], ([], color_map), []);
         };
+      | Derive(concl, prems, rule) =>
+        let concl_id = List.nth(concl.ids, 0);
+        let prems_id = List.nth(prems.ids, 0);
+        let rule_id = List.nth(rule.ids, 0);
+        get_message(
+          ~colorings=
+            DeriveExp.derive_exp_coloring_ids(~concl_id, ~prems_id, ~rule_id),
+          ~format=
+            Some(
+              msg =>
+                Printf.sprintf(
+                  Scanf.format_from_string(msg, "%s%s%s%s"),
+                  Id.to_string(concl_id),
+                  Id.to_string(prems_id),
+                  Id.to_string(rule_id),
+                  Id.to_string(concl_id),
+                ),
+            ),
+          DeriveExp.derives,
+        );
       | If(cond, then_, else_) =>
         let cond_id = List.nth(cond.ids, 0);
         let then_id = List.nth(then_.ids, 0);
diff --git a/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re b/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re
index 79915b42d0..f368760dfd 100644
--- a/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re
+++ b/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re
@@ -77,6 +77,7 @@ let rec precedence = (~show_casts: bool, d: DHExp.t) => {
   | Cast(d1, _, _) =>
     show_casts ? DHDoc_common.precedence_const : precedence'(d1)
   | Ap(_) => DHDoc_common.precedence_Ap
+  | Derive(_, _, _) => DHDoc_common.precedence_Ap
   | ApBuiltin(_) => DHDoc_common.precedence_Ap
   | Cons(_) => DHDoc_common.precedence_Cons
   | ListConcat(_) => DHDoc_common.precedence_Plus
@@ -388,6 +389,13 @@ let mk =
           go'(d2, Ap2),
         );
         DHDoc_common.mk_Ap(doc1, doc2);
+      | Derive(d1, d2, d3) =>
+        let (doc1, doc2, doc3) = (
+          go'(d1, Derive1),
+          go'(d2, Derive2),
+          go'(d3, Derive3),
+        );
+        DHDoc_common.mk_Derive(doc1, doc2, doc3);
       | ApBuiltin(ident, d) =>
         DHDoc_common.mk_Ap(
           text(ident),
diff --git a/src/haz3lweb/view/dhcode/layout/DHDoc_common.re b/src/haz3lweb/view/dhcode/layout/DHDoc_common.re
index 4d3a0ce999..77950ca2b2 100644
--- a/src/haz3lweb/view/dhcode/layout/DHDoc_common.re
+++ b/src/haz3lweb/view/dhcode/layout/DHDoc_common.re
@@ -147,5 +147,8 @@ let mk_Tuple = elts => mk_comma_seq("", "", elts);
 let mk_Ap = (doc1, doc2) =>
   Doc.(hcats([doc1, text("("), doc2, text(")")]));
 
+let mk_Derive = (doc1, doc2, doc3) =>
+  Doc.(hcats([doc1, text("\\"), doc2, text("("), doc3, text(")")]));
+
 let mk_Prj = (targ, n) =>
   Doc.hcats([targ, Delim.projection_dot, Doc.text(string_of_int(n))]);
diff --git a/src/haz3lweb/view/dhcode/layout/DHDoc_common.rei b/src/haz3lweb/view/dhcode/layout/DHDoc_common.rei
index e3da7e68df..e8c1bf4f0d 100644
--- a/src/haz3lweb/view/dhcode/layout/DHDoc_common.rei
+++ b/src/haz3lweb/view/dhcode/layout/DHDoc_common.rei
@@ -103,4 +103,8 @@ let mk_Tuple: list(Pretty.Doc.t('a)) => Pretty.Doc.t('a);
 
 let mk_Ap: (Pretty.Doc.t('a), Pretty.Doc.t('a)) => Pretty.Doc.t('a);
 
+let mk_Derive:
+  (Pretty.Doc.t('a), Pretty.Doc.t('a), Pretty.Doc.t('a)) =>
+  Pretty.Doc.t('a);
+
 let mk_Prj: (Pretty.Doc.t(DHAnnot.t), int) => Pretty.Doc.t(DHAnnot.t);