diff --git a/src/haz3lcore/derivation/DrvElab.re b/src/haz3lcore/derivation/DrvElab.re
index f131b23cce..fad3ddaaa9 100644
--- a/src/haz3lcore/derivation/DrvElab.re
+++ b/src/haz3lcore/derivation/DrvElab.re
@@ -1,5 +1,17 @@
 open DrvSyntax;
 
+let to_list = d =>
+  switch (DrvSyntax.term_of(d)) {
+  | Ctx(ps) => ps
+  | _ => [d]
+  };
+
+let to_ctx = d =>
+  switch (DrvSyntax.term_of(d)) {
+  | Ctx(_) => d
+  | _ => Ctx([d]) |> DrvSyntax.fresh
+  };
+
 let rec elaborate: Drv.t => t =
   fun
   | Jdmt(jdmt) => elab_jdmt(jdmt)
@@ -15,19 +27,7 @@ and elab_jdmt: Drv.Jdmt.t => t =
       | Hole(s) => Hole(TermBase.TypeHole.show(s))
       | Val(e) => Val(elab_exp(e))
       | Eval(e1, e2) => Eval(elab_exp(e1), elab_exp(e2))
-      | Entail(p1, p2) =>
-        Entail(
-          elab_prop(p1)
-          |> (
-            p => {
-              switch (p.term) {
-              | Ctx(_) => p
-              | _ => (Ctx([p]): term) |> IdTagged.fresh
-              };
-            }
-          ),
-          elab_prop(p2),
-        )
+      | Entail(p1, p2) => Entail(elab_prop(p1) |> to_ctx, elab_prop(p2))
       };
     {...jdmt, term};
   }
@@ -48,15 +48,8 @@ and elab_prop: Drv.Prop.t => t =
       | Tuple(ps) =>
         Ctx(
           ps
-          |> List.map(p =>
-               p
-               |> elab_prop
-               |> (
-                 fun
-                 | {term: Ctx(ctx), _} => ctx
-                 | p => [p]
-               )
-             )
+          |> List.map(elab_prop)
+          |> List.map(to_list)
           |> List.concat
           |> List.fold_left(cons_ctx, []),
         )
diff --git a/src/haz3lcore/derivation/DrvSyntax.re b/src/haz3lcore/derivation/DrvSyntax.re
index c076adec7b..cb02f51b76 100644
--- a/src/haz3lcore/derivation/DrvSyntax.re
+++ b/src/haz3lcore/derivation/DrvSyntax.re
@@ -80,7 +80,9 @@ type term =
   | TPat(string)
 and t = IdTagged.t(term);
 
-let fresh = (term: term) => IdTagged.fresh(term);
+let fresh: term => t = IdTagged.fresh;
+
+let term_of: t => term = IdTagged.term_of;
 
 let temp = (term: term) =>
   IdTagged.{term, ids: [Id.invalid], copied: false};
diff --git a/src/haz3lcore/derivation/Rule.re b/src/haz3lcore/derivation/Rule.re
index 0b805bb6ec..2bd9038e7f 100644
--- a/src/haz3lcore/derivation/Rule.re
+++ b/src/haz3lcore/derivation/Rule.re
@@ -280,7 +280,11 @@ type kind =
   | Typing
   | Values
   | Evaluation
-  | PropositionalLogic;
+  | PropositionalLogic(prop_logic_kind)
+and prop_logic_kind =
+  | Assumption
+  | Introduction
+  | Elimination;
 
 let of_kind: t => kind =
   fun
@@ -392,17 +396,17 @@ let of_kind: t => kind =
   | E_Fix
   | E_Roll
   | E_Unroll => Evaluation
-  | Assumption
+  | Assumption => PropositionalLogic(Assumption)
   | And_I
-  | And_E_L
-  | And_E_R
   | Or_I_L
   | Or_I_R
-  | Or_E
   | Implies_I
+  | Truth_I => PropositionalLogic(Introduction)
+  | And_E_L
+  | And_E_R
+  | Or_E
   | Implies_E
-  | Truth_I
-  | Falsity_E => PropositionalLogic;
+  | Falsity_E => PropositionalLogic(Elimination);
 
 [@deriving (show({with_path: false}), sexp, yojson)]
 type sort =
@@ -806,3 +810,26 @@ let all: list(t) = [
   Truth_I,
   Falsity_E,
 ];
+
+let keywords: t => list(string) =
+  rule =>
+    (repr(rule) |> String.split_on_char('-'))
+    @ (
+      switch (of_kind(rule)) {
+      | TypeValidity => ["Type", "Validity", "typ", "tv", "val"]
+      | Synthesis => ["Synthesis", "syn"]
+      | Analysis => ["Analysis", "ana"]
+      | Typing => ["Type", "Typing", "typ"]
+      | Values => ["Values", "val"]
+      | Evaluation => ["Evaluation", "eval"]
+      | PropositionalLogic(prop_logic_kind) =>
+        ["Propositional", "Logic", "prop"]
+        @ (
+          switch (prop_logic_kind) {
+          | Assumption => ["assump", "asm"]
+          | Introduction => ["Introduction", "Intro"]
+          | Elimination => ["Elimination", "Elim"]
+          }
+        )
+      }
+    );
diff --git a/src/haz3lcore/derivation/RuleVerify.re b/src/haz3lcore/derivation/RuleVerify.re
index 4b7f56d5f8..c406c0b0e3 100644
--- a/src/haz3lcore/derivation/RuleVerify.re
+++ b/src/haz3lcore/derivation/RuleVerify.re
@@ -816,6 +816,9 @@ let expect_prems_num: (Rule.t, list(t)) => result(int => t, failure) =
   };
 
 let verify = (rule: Rule.t, prems: list(t), concl: t): result(unit, failure) => {
+  prems |> List.iter(p => print_endline(show(p)));
+  print_endline(show(concl));
+
   let$ prems = expect_prems_num(rule, prems);
   // The following symbols / operators are defined for convenience just
   // under this function.
diff --git a/src/haz3lcore/dynamics/Transition.re b/src/haz3lcore/dynamics/Transition.re
index b21d5965e7..e395d68096 100644
--- a/src/haz3lcore/dynamics/Transition.re
+++ b/src/haz3lcore/dynamics/Transition.re
@@ -252,8 +252,8 @@ module Transition = (EV: EV_MODE) => {
         switch (term) {
         | Hole(s) => Hole(s)
         | Val(e) => Val(go_exp(e))
-        | Eval(e1, e2) => Eval(e1, e2)
-        | Entail(p1, p2) => Entail(p1, p2)
+        | Eval(e1, e2) => Eval(go_exp(e1), go_exp(e2))
+        | Entail(p1, p2) => Entail(go_prop(p1), go_prop(p2))
         };
       term |> rewrap;
     }
@@ -661,12 +661,12 @@ module Transition = (EV: EV_MODE) => {
       Constructor;
     | Derivation(_) =>
       let. _ = otherwise(env, d);
-      Step({
-        expr: replace_drv_abbrs(env, d),
-        state_update,
-        kind: InvalidStep,
-        is_value: true,
-      });
+      let d' = replace_drv_abbrs(env, d);
+      if (DHExp.fast_equal(d, d')) {
+        Constructor;
+      } else {
+        Step({expr: d', state_update, kind: CompleteClosure, is_value: true});
+      };
     | If(c, d1, d2) =>
       let. _ = otherwise(env, c => If(c, d1, d2) |> rewrap)
       and. c' =
diff --git a/src/haz3lcore/lang/Form.re b/src/haz3lcore/lang/Form.re
index 0fe7fc48d9..8764718971 100644
--- a/src/haz3lcore/lang/Form.re
+++ b/src/haz3lcore/lang/Form.re
@@ -373,12 +373,12 @@ let forms: list((string, t)) = [
   ),
   ("if_", mk(ds, ["if", "then", "else"], mk_pre(P.if_, Exp, [Exp, Exp]))),
   // Drv
-  // ("of_alfa_typ", mk(ds, ["of_Typ", "end"], mk_op(Exp, [Drv(Typ)]))),
-  // ("of_alfa_exp", mk(ds, ["of_Exp", "end"], mk_op(Exp, [Drv(Exp)]))),
-  // ("of_alfa_pat", mk(ds, ["of_Pat", "end"], mk_op(Exp, [Drv(Pat)]))),
-  // ("of_alfa_tpat", mk(ds, ["of_TPat", "end"], mk_op(Exp, [Drv(TPat)]))),
-  // ("of_prop", mk(ds, ["of_Prop", "end"], mk_op(Exp, [Drv(Prop)]))),
-  // ("of_jdmt", mk(ds, ["of_Jdmt", "end"], mk_op(Exp, [Drv(Jdmt)]))),
+  ("of_alfa_typ", mk(ds, ["of_Typ", "end"], mk_op(Exp, [Drv(Typ)]))),
+  ("of_alfa_exp", mk(ds, ["of_Exp", "end"], mk_op(Exp, [Drv(Exp)]))),
+  ("of_alfa_pat", mk(ds, ["of_Pat", "end"], mk_op(Exp, [Drv(Pat)]))),
+  ("of_alfa_tpat", mk(ds, ["of_TPat", "end"], mk_op(Exp, [Drv(TPat)]))),
+  ("of_prop", mk(ds, ["of_Prop", "end"], mk_op(Exp, [Drv(Prop)]))),
+  ("of_jdmt", mk(ds, ["of_Jdmt", "end"], mk_op(Exp, [Drv(Jdmt)]))),
   (
     "prop_alias",
     mk(ds, ["prop", "=", "in"], mk_pre(P.let_, Exp, [Pat, Drv(Prop)])),
diff --git a/src/haz3lcore/statics/MakeTerm.re b/src/haz3lcore/statics/MakeTerm.re
index 2d91cd67fa..af9f14c53a 100644
--- a/src/haz3lcore/statics/MakeTerm.re
+++ b/src/haz3lcore/statics/MakeTerm.re
@@ -384,7 +384,6 @@ and alfa_tpat_term: unsorted => (Drv.TPat.term, list(Id.t)) = {
 
 and exp = unsorted => {
   let (term, inner_ids) = exp_term(unsorted);
-  print_endline("term: " ++ TermBase.Exp.show_term(term));
   switch (term) {
   | MultiHole([Drv(_), ..._]) =>
     let (term, inner_ids) = jdmt_term(unsorted);
@@ -428,6 +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_TPat", "end"], [Drv(TPat(tp))]) =>
+        ret(Derivation(TPat(tp)))
+      | (["of_Prop", "end"], [Drv(Prop(p))]) => ret(Derivation(Prop(p)))
+      | (["of_Jdmt", "end"], [Drv(Jdmt(j))]) => ret(Derivation(Jdmt(j)))
       | ([t], []) when t != " " && !Form.is_explicit_hole(t) =>
         ret(Invalid(t))
       | _ => ret(hole(tm))
diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re
index fb50b93046..77b520131d 100644
--- a/src/haz3lcore/statics/Statics.re
+++ b/src/haz3lcore/statics/Statics.re
@@ -217,11 +217,7 @@ and drv_to_info_map =
     | Tuple(_) when !can_tuple =>
       m |> add(Prop(prop), Prop({...info, status: InHole(NotAllowTuple)}))
     | Tuple(ps) =>
-      List.fold_left(
-        (m, p) => m |> go_prop(p, ~can_tuple=false) |> snd,
-        m,
-        ps,
-      )
+      List.fold_left((m, p) => m |> go_prop(p, ~can_tuple) |> snd, m, ps)
       |> add'
     | Abbr(p) =>
       m
diff --git a/src/haz3lweb/view/Page.re b/src/haz3lweb/view/Page.re
index 33c4d5014d..508303f40e 100644
--- a/src/haz3lweb/view/Page.re
+++ b/src/haz3lweb/view/Page.re
@@ -100,7 +100,7 @@ let main_view =
       ~explainThisModel,
       Code(cursor_info),
     );
-  let (editors_view, cursor_info) =
+  let (editors_view, cursor_info, cursor_info_for_sidebar) =
     switch (editors) {
     | Scratch(idx, _) =>
       let result_key = ScratchSlide.scratch_key(string_of_int(idx));
@@ -114,7 +114,7 @@ let main_view =
           ~result_key,
           editor,
         );
-      (view, ExplainThis.Code(cursor_info));
+      (view, cursor_info, ExplainThis.Code(cursor_info));
     | Documentation(name, _) =>
       let result_key = ScratchSlide.scratch_key(name);
       let view =
@@ -131,7 +131,7 @@ let main_view =
         SlideContent.get_content(editors)
         |> Option.map(i => div(~attrs=[Attr.id("slide")], [i]))
         |> Option.to_list;
-      (info @ view, ExplainThis.Code(cursor_info));
+      (info @ view, cursor_info, ExplainThis.Code(cursor_info));
     | Exercises(_, _, exercise) =>
       /* Note the exercises mode uses a seperate path to calculate
        * statics and dynamics via stitching together multiple editors */
@@ -151,7 +151,7 @@ let main_view =
           ~explainThisModel,
           Code(cursor_info),
         );
-      let (view, cursor_info) =
+      let (view, cursor_info') =
         ExerciseMode.view(
           ~inject,
           ~ui_state,
@@ -162,7 +162,7 @@ let main_view =
           ~exercise,
           ~cursor_info=Code(cursor_info),
         );
-      (view, cursor_info);
+      (view, cursor_info, cursor_info');
     };
 
   let sidebar =
@@ -172,11 +172,9 @@ let main_view =
           ~ui_state,
           ~settings,
           ~explainThisModel,
-          cursor_info // Now a {info, results}
+          cursor_info_for_sidebar,
         )
       : div([]);
-  let cursor_info =
-    Indicated.ci_of(editor.state.zipper, editor.state.meta.statics.info_map);
   let bottom_bar =
     CursorInspector.view(~inject, ~settings, editor, cursor_info);
   [
diff --git a/src/haz3lweb/view/exercise/NinjaKeysRules.re b/src/haz3lweb/view/exercise/NinjaKeysRules.re
index 8841550169..51caa63e59 100644
--- a/src/haz3lweb/view/exercise/NinjaKeysRules.re
+++ b/src/haz3lweb/view/exercise/NinjaKeysRules.re
@@ -39,6 +39,7 @@ let from_rule =
         "id": Js.readonly_prop(string),
         "title": Js.readonly_prop(string),
         "section": Js.readonly_prop(Js.optdef(string)),
+        "keywords": Js.readonly_prop(string),
       } => {
   [%js
    {
@@ -48,7 +49,8 @@ let from_rule =
        Js.Optdef.option(
          Some(Haz3lcore.Rule.show_kind(Haz3lcore.Rule.of_kind(rule))),
        );
-     val handler = () => update_rule(rule) |> schedule_action
+     val handler = () => update_rule(rule) |> schedule_action;
+     val keywords = Haz3lcore.Rule.keywords(rule) |> String.concat(" ")
    }];
 };