diff --git a/lib/sml-dependent-lcf b/lib/sml-dependent-lcf
index 63d0ca6ac..856234846 160000
--- a/lib/sml-dependent-lcf
+++ b/lib/sml-dependent-lcf
@@ -1 +1 @@
-Subproject commit 63d0ca6acf279f562da7e7b3a80ab5910fad88cd
+Subproject commit 856234846be7e0d30a8e8fbc48efbd1b27986377
diff --git a/lib/sml-typed-abts b/lib/sml-typed-abts
index 7c50bcd91..cff9682f9 160000
--- a/lib/sml-typed-abts
+++ b/lib/sml-typed-abts
@@ -1 +1 @@
-Subproject commit 7c50bcd911bd669561206f06f4cfe1c6e65eea18
+Subproject commit cff9682f9da46acd0797a527dd9608f5c4b0fa9f
diff --git a/src/redprl/judgment.fun b/src/redprl/judgment.fun
index 373c5f9f4..d2a8b0981 100644
--- a/src/redprl/judgment.fun
+++ b/src/redprl/judgment.fun
@@ -1,21 +1,25 @@
 functor SequentJudgment
   (structure S : SEQUENT where type 'a CJ.Tm.O.Ar.Vl.Sp.t = 'a list
-   structure TermPrinter : SHOW where type t = S.CJ.Tm.abt) : LCF_JUDGMENT =
+   structure TermPrinter : SHOW where type t = S.CJ.Tm.abt) : LCF_BINDING_JUDGMENT =
 struct
   structure CJ = S.CJ
   structure Tm = CJ.Tm
   type sort = Tm.valence
   type env = Tm.metaenv
   type jdg = Tm.abt S.jdg
+  type symenv = Tm.symenv
+  type varenv = Tm.varenv
 
   val subst = S.map o Tm.substMetaenv
   val eq = S.eq
   val toString = S.toString TermPrinter.toString
 
+  val substSymenv = S.map o Tm.substSymenv
+  val substVarenv = S.map o Tm.substVarenv
 
   local
     open S
-    infix >> |>
+    infix >>
   in
     val rec sort =
       fn H >> catjdg => (([],[]), CJ.synthesis catjdg)
@@ -25,12 +29,6 @@ struct
            in
              List.nth (vls, k)
            end
-       | (U, G) |> jdg =>
-           let
-             val ((sigmas, taus), tau) = sort jdg
-           in
-             ((List.map #2 U @ sigmas, List.map #2 G @ taus), tau)
-           end
   end
 end
 
diff --git a/src/redprl/lcf_model.fun b/src/redprl/lcf_model.fun
index f353c6092..1e5d15afe 100644
--- a/src/redprl/lcf_model.fun
+++ b/src/redprl/lcf_model.fun
@@ -19,16 +19,16 @@ struct
   fun interpret (sign, env) rule =
     case out rule of
        O.MONO O.RULE_ID $ _ => (fn _ => Lcf.idn)
-     | O.MONO O.RULE_EVAL_GOAL $ _ => Rules.Lift (Rules.CEquiv.EvalGoal sign)
-     | O.MONO O.RULE_CEQUIV_REFL $ _ => Rules.Lift (Rules.CEquiv.Refl)
-     | O.MONO O.RULE_AUTO_STEP $ _ => Rules.Lift (Rules.AutoStep sign)
-     | O.POLY (O.RULE_HYP z) $ _ => Rules.Lift (Rules.Hyp.Project z)
-     | O.POLY (O.RULE_ELIM z) $ _ => Rules.Lift (Rules.Elim sign z)
-     | O.MONO O.RULE_WITNESS $ [_ \ tm] => Rules.Lift (Rules.Truth.Witness tm)
-     | O.MONO O.RULE_HEAD_EXP $ _ => Rules.Lift (Rules.Computation.EqHeadExpansion sign)
-     | O.MONO O.RULE_SYMMETRY $ _ => Rules.Lift Rules.Equality.Symmetry
-     | O.MONO O.RULE_CUT $ [_ \ catjdg] => Rules.Lift (Rules.Cut (RedPrlCategoricalJudgment.fromAbt catjdg))
-     | O.MONO (O.RULE_LEMMA _) $ [_ \ thm] => Rules.Lift (Rules.Lemma thm)
+     | O.MONO O.RULE_EVAL_GOAL $ _ => Rules.CEquiv.EvalGoal sign
+     | O.MONO O.RULE_CEQUIV_REFL $ _ => Rules.CEquiv.Refl
+     | O.MONO O.RULE_AUTO_STEP $ _ => Rules.AutoStep sign
+     | O.POLY (O.RULE_HYP z) $ _ => Rules.Hyp.Project z
+     | O.POLY (O.RULE_ELIM z) $ _ => Rules.Elim sign z
+     | O.MONO O.RULE_WITNESS $ [_ \ tm] => Rules.Truth.Witness tm
+     | O.MONO O.RULE_HEAD_EXP $ _ => Rules.Computation.EqHeadExpansion sign
+     | O.MONO O.RULE_SYMMETRY $ _ => Rules.Equality.Symmetry
+     | O.MONO O.RULE_CUT $ [_ \ catjdg] => Rules.Cut (RedPrlCategoricalJudgment.fromAbt catjdg)
+     | O.MONO (O.RULE_LEMMA _) $ [_ \ thm] => Rules.Lemma thm
      | _ => raise E.error [E.% "Invalid rule", E.! rule]
 
   fun rule (sign, env) rule alpha goal =
diff --git a/src/redprl/machine.sml b/src/redprl/machine.sml
index db015cab6..b41c3b91f 100644
--- a/src/redprl/machine.sml
+++ b/src/redprl/machine.sml
@@ -115,10 +115,7 @@ struct
       O.MONO O.MTAC_PROGRESS $$ [([],[]) \ mt]
 
     fun multirepeat mt =
-      let
-      in
         O.MONO O.MTAC_REPEAT $$ [([],[]) \ mt]
-      end
 
     fun cut jdg =
       O.MONO O.RULE_CUT $$ [([],[]) \ jdg]
diff --git a/src/redprl/refiner.fun b/src/redprl/refiner.fun
index b83075db3..7d5978a78 100644
--- a/src/redprl/refiner.fun
+++ b/src/redprl/refiner.fun
@@ -8,9 +8,10 @@ struct
   type catjdg = abt CJ.jdg
 
   infixr @@
-  infix 1 |>
+  infix 1 ||
   infix 2 >> >: $$ $# // \ @>
 
+  val op|| = Lcf.||
   fun #> (psi, m) = Lcf.|> (psi, abtToAbs m)
   infix #>
 
@@ -24,7 +25,7 @@ struct
       let
         val _ = RedPrlLog.trace "CEquiv.EvalGoal"
         val H >> CJ.CEQUIV (m, n) = jdg
-        val (goal, hole) = makeGoal @@ H >> CJ.CEQUIV (Machine.eval sign m, Machine.eval sign n)
+        val (goal, hole) = makeGoal @@ ([],[]) || H >> CJ.CEQUIV (Machine.eval sign m, Machine.eval sign n)
       in
         T.empty >: goal
           #> hole [] []
@@ -94,15 +95,15 @@ struct
         val Hbase = Hyps.modifyAfter z (CJ.map (substVar (base, z))) H
         val cbase = substVar (base, z) cz
 
-        val (goalB, holeB) = makeGoal @@ Hbase >> CJ.TRUE cbase
-        val (goalL, holeL) = makeGoal @@ ([(u, P.DIM)], []) |> Hyps.modifyAfter z (CJ.map (substVar (loop, z))) H >> CJ.TRUE (substVar (loop, z) cz)
+        val (goalB, holeB) = makeGoal @@ ([],[]) || Hbase >> CJ.TRUE cbase
+        val (goalL, holeL) = makeGoal @@ ([(u, P.DIM)], []) || Hyps.modifyAfter z (CJ.map (substVar (loop, z))) H >> CJ.TRUE (substVar (loop, z) cz)
 
         val b = holeB [][]
         val l0 = holeL [(P.APP P.DIM0, P.DIM)] []
         val l1 = holeL [(P.APP P.DIM1, P.DIM)] []
 
-        val (goalCoh0, _) = makeGoal @@ Hbase >> CJ.EQ ((l0, b), cbase)
-        val (goalCoh1, _) = makeGoal @@ Hbase >> CJ.EQ ((l1, b), cbase)
+        val (goalCoh0, _) = makeGoal @@ ([],[]) || Hbase >> CJ.EQ ((l0, b), cbase)
+        val (goalCoh1, _) = makeGoal @@ ([],[]) || Hbase >> CJ.EQ ((l1, b), cbase)
 
         val psi = T.empty >: goalB >: goalL >: goalCoh0 >: goalCoh1
 
@@ -135,12 +136,12 @@ struct
 
         val S1 = Syn.into Syn.S1
 
-        val (goalCz, _) = makeGoal @@ ([], [(z, O.EXP)]) |> H @> (z, CJ.TRUE S1) >> CJ.EQ_TYPE (c0z, c1z)
-        val (goalM, _) = makeGoal @@ H >> CJ.EQ ((m0, m1), S1)
-        val (goalB, _) = makeGoal @@ H >> CJ.EQ ((b0, b1), cbase)
-        val (goalL, _) = makeGoal @@ H >> CJ.EQ ((l0u, l1u), cloop)
-        val (goalL00, _) = makeGoal @@ H >> CJ.EQ ((l00, b0), cbase)
-        val (goalL01, _) = makeGoal @@ H >> CJ.EQ ((l01, b0), cbase)
+        val (goalCz, _) = makeGoal @@ ([], [(z, O.EXP)]) || H @> (z, CJ.TRUE S1) >> CJ.EQ_TYPE (c0z, c1z)
+        val (goalM, _) = makeGoal @@ ([],[]) || H >> CJ.EQ ((m0, m1), S1)
+        val (goalB, _) = makeGoal @@ ([],[]) || H >> CJ.EQ ((b0, b1), cbase)
+        val (goalL, _) = makeGoal @@ ([],[]) || H >> CJ.EQ ((l0u, l1u), cloop)
+        val (goalL00, _) = makeGoal @@ ([],[]) || H >> CJ.EQ ((l00, b0), cbase)
+        val (goalL01, _) = makeGoal @@ ([],[]) || H >> CJ.EQ ((l01, b0), cbase)
 
         val psi = T.empty >: goalCz >: goalM >: goalB >: goalL >: goalL00 >: goalL01
       in
@@ -194,8 +195,8 @@ struct
         val tt = Syn.into Syn.TT
         val ff = Syn.into Syn.FF
 
-        val (goalT, holeT) = makeGoal @@ Hyps.modifyAfter z (CJ.map (substVar (tt, z))) H >> CJ.TRUE (substVar (tt, z) cz)
-        val (goalF, holeF) = makeGoal @@ Hyps.modifyAfter z (CJ.map (substVar (ff, z))) H >> CJ.TRUE (substVar (ff, z) cz)
+        val (goalT, holeT) = makeGoal @@ ([],[]) || Hyps.modifyAfter z (CJ.map (substVar (tt, z))) H >> CJ.TRUE (substVar (tt, z) cz)
+        val (goalF, holeF) = makeGoal @@ ([],[]) || Hyps.modifyAfter z (CJ.map (substVar (ff, z))) H >> CJ.TRUE (substVar (ff, z) cz)
 
         val psi = T.empty >: goalT >: goalF
         val ztm = Syn.into @@ Syn.VAR (z, O.EXP)
@@ -221,11 +222,11 @@ struct
         val c0ff = substVar (Syn.into Syn.FF, x) c0x
         val c0m0 = substVar (m0, x) c0x
 
-        val (goalTy, _) = makeGoal @@ ([], [(z, O.EXP)]) |> H @> (z, CJ.TRUE @@ Syn.into Syn.BOOL) >> CJ.EQ_TYPE (c0z, c1z)
-        val (goalTy', _) = makeGoal @@ H >> CJ.EQ_TYPE (c0m0, c)
-        val (goalM, _) = makeGoal @@ H >> CJ.EQ ((m0, m1), Syn.into Syn.BOOL)
-        val (goalT, _) = makeGoal @@ H >> CJ.EQ ((t0, t1), c0tt)
-        val (goalF, _) = makeGoal @@ H >> CJ.EQ ((f0, f1), c0ff)
+        val (goalTy, _) = makeGoal @@ ([], [(z, O.EXP)]) || H @> (z, CJ.TRUE @@ Syn.into Syn.BOOL) >> CJ.EQ_TYPE (c0z, c1z)
+        val (goalTy', _) = makeGoal @@ ([],[]) || H >> CJ.EQ_TYPE (c0m0, c)
+        val (goalM, _) = makeGoal @@ ([],[]) || H >> CJ.EQ ((m0, m1), Syn.into Syn.BOOL)
+        val (goalT, _) = makeGoal @@ ([],[]) || H >> CJ.EQ ((t0, t1), c0tt)
+        val (goalF, _) = makeGoal @@ ([],[]) || H >> CJ.EQ ((f0, f1), c0ff)
         val psi = T.empty >: goalTy >: goalM >: goalT >: goalF
       in
         psi #> trivial
@@ -278,8 +279,8 @@ struct
         val tt = Syn.into Syn.TT
         val ff = Syn.into Syn.FF
 
-        val (goalT, holeT) = makeGoal @@ Hyps.modifyAfter z (CJ.map (substVar (tt, z))) H >> CJ.TRUE (substVar (tt, z) cz)
-        val (goalF, holeF) = makeGoal @@ Hyps.modifyAfter z (CJ.map (substVar (ff, z))) H >> CJ.TRUE (substVar (ff, z) cz)
+        val (goalT, holeT) = makeGoal @@ ([],[]) || Hyps.modifyAfter z (CJ.map (substVar (tt, z))) H >> CJ.TRUE (substVar (tt, z) cz)
+        val (goalF, holeF) = makeGoal @@ ([],[]) || Hyps.modifyAfter z (CJ.map (substVar (ff, z))) H >> CJ.TRUE (substVar (ff, z) cz)
 
         val psi = T.empty >: goalT >: goalF
         val ztm = Syn.into @@ Syn.VAR (z, O.EXP)
@@ -297,9 +298,9 @@ struct
         val Syn.S_IF (m0, (t0, f0)) = Syn.out if0
         val Syn.S_IF (m1, (t1, f1)) = Syn.out if1
 
-        val (goalM, _) = makeGoal @@ H >> CJ.EQ ((m0, m1), Syn.into Syn.S_BOOL)
-        val (goalT, _) = makeGoal @@ H >> CJ.EQ ((t0, t1), c)
-        val (goalF, _) = makeGoal @@ H >> CJ.EQ ((f0, f1), c)
+        val (goalM, _) = makeGoal @@ ([],[]) || H >> CJ.EQ ((m0, m1), Syn.into Syn.S_BOOL)
+        val (goalT, _) = makeGoal @@ ([],[]) || H >> CJ.EQ ((t0, t1), c)
+        val (goalF, _) = makeGoal @@ ([],[]) || H >> CJ.EQ ((f0, f1), c)
         val psi = T.empty >: goalM >: goalT >: goalF
       in
         psi #> trivial
@@ -317,10 +318,10 @@ struct
         val tt = Syn.into Syn.TT
         val ff = Syn.into Syn.FF
 
-        val (goalM0, _) = makeGoal @@ H >> CJ.MEM (m0z, cz)
-        val (goalM1, _) = makeGoal @@ H >> CJ.MEM (m1z, cz)
-        val (goalT, _) = makeGoal @@ Hyps.modifyAfter z (CJ.map (substVar (tt, z))) H >> CJ.map (substVar (tt, z)) catjdg
-        val (goalF, _) = makeGoal @@ Hyps.modifyAfter z (CJ.map (substVar (ff, z))) H >> CJ.map (substVar (ff, z)) catjdg
+        val (goalM0, _) = makeGoal @@ ([],[]) || H >> CJ.MEM (m0z, cz)
+        val (goalM1, _) = makeGoal @@ ([],[]) || H >> CJ.MEM (m1z, cz)
+        val (goalT, _) = makeGoal @@ ([],[]) || Hyps.modifyAfter z (CJ.map (substVar (tt, z))) H >> CJ.map (substVar (tt, z)) catjdg
+        val (goalF, _) = makeGoal @@ ([],[]) || Hyps.modifyAfter z (CJ.map (substVar (ff, z))) H >> CJ.map (substVar (ff, z)) catjdg
 
         val psi = T.empty >: goalM0 >: goalM1 >: goalT >: goalF
       in
@@ -344,8 +345,8 @@ struct
         val b0z = substVar (ztm, x) b0x
         val b1z = substVar (ztm, y) b1y
 
-        val (goal1, _) = makeGoal @@ H >> CJ.EQ_TYPE (a0, a1)
-        val (goal2, _) = makeGoal @@ H @> (z, CJ.TRUE a0) >> CJ.EQ_TYPE (b0z, b1z)
+        val (goal1, _) = makeGoal @@ ([],[]) || H >> CJ.EQ_TYPE (a0, a1)
+        val (goal2, _) = makeGoal @@ ([],[]) || H @> (z, CJ.TRUE a0) >> CJ.EQ_TYPE (b0z, b1z)
       in
         T.empty >: goal1 >: goal2
           #> trivial
@@ -365,9 +366,9 @@ struct
         val ztm = Syn.into @@ Syn.VAR (z, O.EXP)
         val bz = substVar (ztm, x) bx
 
-        val (goal1, _) = makeGoal @@ H >> CJ.EQ ((m0, m1), a)
-        val (goal2, _) = makeGoal @@ H >> CJ.EQ ((n0, n1), substVar (m0, x) bx)
-        val (goalFam, _) = makeGoal @@ ([], [(z, O.EXP)]) |> H @> (z, CJ.TRUE a) >> CJ.TYPE bz
+        val (goal1, _) = makeGoal @@ ([],[]) || H >> CJ.EQ ((m0, m1), a)
+        val (goal2, _) = makeGoal @@ ([],[]) || H >> CJ.EQ ((n0, n1), substVar (m0, x) bx)
+        val (goalFam, _) = makeGoal @@ ([], [(z, O.EXP)]) || H @> (z, CJ.TRUE a) >> CJ.TYPE bz
       in
         T.empty >: goal1 >: goal2 >: goalFam
           #> trivial
@@ -380,8 +381,8 @@ struct
         val Syn.DPROD (a, x, bx) = Syn.out dprod
 
         val m' = Syn.into @@ Syn.PAIR (Syn.into @@ Syn.FST m, Syn.into @@ Syn.SND m)
-        val (goal1, _) = makeGoal @@ H >> CJ.MEM (m, dprod)
-        val (goal2, _) = makeGoal @@ H >> CJ.EQ ((m', n), dprod)
+        val (goal1, _) = makeGoal @@ ([],[]) || H >> CJ.MEM (m, dprod)
+        val (goal2, _) = makeGoal @@ ([],[]) || H >> CJ.EQ ((m', n), dprod)
       in
         T.empty >: goal1 >: goal2
           #> trivial
@@ -394,10 +395,10 @@ struct
         val Syn.FST m0 = Syn.out fst0
         val Syn.FST m1 = Syn.out fst1
 
-        val (goalTy, holeTy) = makeGoal @@ H >> CJ.SYNTH m0
-        val (goalTyA, holeTyA) = makeGoal @@ MATCH (O.MONO O.DPROD, 0, holeTy [] [])
-        val (goalEq, _) = makeGoal @@ H >> CJ.EQ ((m0, m1), holeTy [] [])
-        val (goalEqTy, _) = makeGoal @@ H >> CJ.EQ_TYPE (holeTyA [] [], ty)
+        val (goalTy, holeTy) = makeGoal @@ ([],[]) || H >> CJ.SYNTH m0
+        val (goalTyA, holeTyA) = makeGoal @@ ([],[]) || MATCH (O.MONO O.DPROD, 0, holeTy [] [])
+        val (goalEq, _) = makeGoal @@ ([],[]) || H >> CJ.EQ ((m0, m1), holeTy [] [])
+        val (goalEqTy, _) = makeGoal @@ ([],[]) || H >> CJ.EQ_TYPE (holeTyA [] [], ty)
       in
         T.empty >: goalTy >: goalTyA >: goalEq >: goalEqTy
           #> trivial
@@ -410,10 +411,10 @@ struct
         val Syn.SND m0 = Syn.out snd0
         val Syn.SND m1 = Syn.out snd1
 
-        val (goalTy, holeTy) = makeGoal @@ H >> CJ.SYNTH m0
-        val (goalTyB, holeTyB) = makeGoal @@ MATCH (O.MONO O.DPROD, 1, holeTy [] [])
-        val (goalEq, _) = makeGoal @@ H >> CJ.EQ ((m0, m1), holeTy [] [])
-        val (goalEqTy, _) = makeGoal @@ H >> CJ.EQ_TYPE (holeTyB [] [Syn.into @@ Syn.FST m0], ty)
+        val (goalTy, holeTy) = makeGoal @@ ([],[]) || H >> CJ.SYNTH m0
+        val (goalTyB, holeTyB) = makeGoal @@ ([],[]) || MATCH (O.MONO O.DPROD, 1, holeTy [] [])
+        val (goalEq, _) = makeGoal @@ ([],[]) || H >> CJ.EQ ((m0, m1), holeTy [] [])
+        val (goalEqTy, _) = makeGoal @@ ([],[]) || H >> CJ.EQ_TYPE (holeTyB [] [Syn.into @@ Syn.FST m0], ty)
       in
         T.empty >: goalTy >: goalTyB >: goalEq >: goalEqTy
           #> trivial
@@ -429,9 +430,9 @@ struct
         val ztm = Syn.into @@ Syn.VAR (z, O.EXP)
         val bz = substVar (ztm, x) bx
 
-        val (goal1, hole1) = makeGoal @@ H >> CJ.TRUE a
-        val (goal2, hole2) = makeGoal @@ H >> CJ.TRUE (substVar (hole1 [] [], x) bx)
-        val (goalFam, _) = makeGoal @@ ([], [(z, O.EXP)]) |> H @> (z, CJ.TRUE a) >> CJ.TYPE bz
+        val (goal1, hole1) = makeGoal @@ ([],[]) || H >> CJ.TRUE a
+        val (goal2, hole2) = makeGoal @@ ([],[]) || H >> CJ.TRUE (substVar (hole1 [] [], x) bx)
+        val (goalFam, _) = makeGoal @@ ([], [(z, O.EXP)]) || H @> (z, CJ.TRUE a) >> CJ.TYPE bz
         val psi = T.empty >: goal1 >: goal2 >: goalFam
         val pair = Syn.into @@ Syn.PAIR (hole1 [] [], hole2 [] [])
       in
@@ -460,7 +461,7 @@ struct
         val (goal, hole) =
           makeGoal
             @@ ([], [(z1, O.EXP), (z2, O.EXP)])
-            |> Hyps.modifyAfter z (CJ.map (substVar (pair, z))) H''
+            || Hyps.modifyAfter z (CJ.map (substVar (pair, z))) H''
             >> CJ.TRUE (substVar (pair, z) cz)
 
         val psi = T.empty >: goal
@@ -488,8 +489,8 @@ struct
         val b0z = substVar (ztm, x) b0x
         val b1z = substVar (ztm, y) b1y
 
-        val (goal1, _) = makeGoal @@ H >> CJ.EQ_TYPE (a0, a1)
-        val (goal2, _) = makeGoal @@ H @> (z, CJ.TRUE a0) >> CJ.EQ_TYPE (b0z, b1z)
+        val (goal1, _) = makeGoal @@ ([],[]) || H >> CJ.EQ_TYPE (a0, a1)
+        val (goal2, _) = makeGoal @@ ([],[]) || H @> (z, CJ.TRUE a0) >> CJ.EQ_TYPE (b0z, b1z)
       in
         T.empty >: goal1 >: goal2
           #> trivial
@@ -512,8 +513,8 @@ struct
         val m1w = substVar (wtm, y) m1y
         val bw = substVar (wtm, z) bz
 
-        val (goal1, _) = makeGoal @@ ([],[(w, O.EXP)]) |> H @> (w, CJ.TRUE a) >> CJ.EQ ((m0w, m1w), bw)
-        val (goal2, _) = makeGoal @@ H >> CJ.TYPE a
+        val (goal1, _) = makeGoal @@ ([],[(w, O.EXP)]) || H @> (w, CJ.TRUE a) >> CJ.EQ ((m0w, m1w), bw)
+        val (goal2, _) = makeGoal @@ ([],[]) || H >> CJ.TYPE a
       in
         T.empty >: goal1 >: goal2
           #> trivial
@@ -529,8 +530,8 @@ struct
         val ztm = Syn.into @@ Syn.VAR (z, O.EXP)
         val bz = substVar (ztm, x) bx
 
-        val (tyGoal, _) = makeGoal @@ H >> CJ.TYPE a
-        val (goal, hole) = makeGoal @@ ([],[(z, O.EXP)]) |> H @> (z, CJ.TRUE a) >> CJ.TRUE bz
+        val (tyGoal, _) = makeGoal @@ ([],[]) || H >> CJ.TYPE a
+        val (goal, hole) = makeGoal @@ ([],[(z, O.EXP)]) || H @> (z, CJ.TRUE a) >> CJ.TRUE bz
 
         val psi = T.empty >: goal >: tyGoal
         val lam = Syn.into @@ Syn.LAM (z, hole [] [ztm])
@@ -548,8 +549,8 @@ struct
 
         val xtm = Syn.into @@ Syn.VAR (x, O.EXP)
         val m' = Syn.into @@ Syn.LAM (x, Syn.into @@ Syn.AP (m, xtm))
-        val (goal1, _) = makeGoal @@ H >> CJ.MEM (m, dfun)
-        val (goal2, _) = makeGoal @@ H >> CJ.EQ ((m', n), dfun)
+        val (goal1, _) = makeGoal @@ ([],[]) || H >> CJ.MEM (m, dfun)
+        val (goal2, _) = makeGoal @@ ([],[]) || H >> CJ.EQ ((m', n), dfun)
       in
         T.empty >: goal1 >: goal2
           #> trivial
@@ -561,7 +562,7 @@ struct
         val H >> CJ.TRUE cz = jdg
         val CJ.TRUE dfun = Hyps.lookup H z
         val Syn.DFUN (a, x, bx) = Syn.out dfun
-        val (goal1, hole1) = makeGoal @@ H >> CJ.TRUE a
+        val (goal1, hole1) = makeGoal @@ ([],[]) || H >> CJ.TRUE a
 
         val u = alpha 0
         val v = alpha 1
@@ -574,7 +575,7 @@ struct
         val H' = Hyps.empty @> (u, CJ.TRUE b') @> (v, CJ.EQ ((utm, aptm), b'))
         val H'' = Hyps.interposeAfter H z H'
 
-        val (goal2, hole2) = makeGoal @@ ([], [(u, O.EXP), (v, O.TRIV)]) |> H'' >> CJ.TRUE cz
+        val (goal2, hole2) = makeGoal @@ ([], [(u, O.EXP), (v, O.TRIV)]) || H'' >> CJ.TRUE cz
 
         val psi = T.empty >: goal1 >: goal2
         val aptm = Syn.into @@ Syn.AP (ztm, hole1 [] [])
@@ -589,12 +590,12 @@ struct
         val Syn.AP (m0, n0) = Syn.out ap0
         val Syn.AP (m1, n1) = Syn.out ap1
 
-        val (goalDFun0, holeDFun0) = makeGoal @@ H >> CJ.SYNTH m0
-        val (goalDFun1, holeDFun1) = makeGoal @@ H >> CJ.SYNTH m1
-        val (goalDFunEq, _) = makeGoal @@ H >> CJ.EQ_TYPE (holeDFun0 [] [], holeDFun1 [] [])
-        val (goalDom, holeDom) = makeGoal @@ MATCH (O.MONO O.DFUN, 0, holeDFun0 [] [])
-        val (goalM, _) = makeGoal @@ H >> CJ.EQ ((m0, m1), holeDFun0 [] [])
-        val (goalN, _) = makeGoal @@ H >> CJ.EQ ((n0, n1), holeDom [] [])
+        val (goalDFun0, holeDFun0) = makeGoal @@ ([],[]) || H >> CJ.SYNTH m0
+        val (goalDFun1, holeDFun1) = makeGoal @@ ([],[]) || H >> CJ.SYNTH m1
+        val (goalDFunEq, _) = makeGoal @@ ([],[]) || H >> CJ.EQ_TYPE (holeDFun0 [] [], holeDFun1 [] [])
+        val (goalDom, holeDom) = makeGoal @@ ([],[]) || MATCH (O.MONO O.DFUN, 0, holeDFun0 [] [])
+        val (goalM, _) = makeGoal @@ ([],[]) || H >> CJ.EQ ((m0, m1), holeDFun0 [] [])
+        val (goalN, _) = makeGoal @@ ([],[]) || H >> CJ.EQ ((n0, n1), holeDom [] [])
       in
         T.empty >: goalDFun0 >: goalDFun1 >: goalDFunEq >: goalDom >: goalM >: goalN
           #> trivial
@@ -615,9 +616,9 @@ struct
         val a00 = substSymbol (P.APP P.DIM0, u) a0u
         val a01 = substSymbol (P.APP P.DIM1, u) a0u
 
-        val (tyGoal, _) = makeGoal @@ H >> CJ.EQ_TYPE (a0u, a1u)
-        val (goal0, _) = makeGoal @@ H >> CJ.EQ ((m0, m1), a00)
-        val (goal1, _) = makeGoal @@ H >> CJ.EQ ((n0, n1), a01)
+        val (tyGoal, _) = makeGoal @@ ([],[]) || H >> CJ.EQ_TYPE (a0u, a1u)
+        val (goal0, _) = makeGoal @@ ([],[]) || H >> CJ.EQ ((m0, m1), a00)
+        val (goal1, _) = makeGoal @@ ([],[]) || H >> CJ.EQ ((n0, n1), a01)
       in
         T.empty >: tyGoal >: goal0 >: goal1
           #> trivial
@@ -633,12 +634,12 @@ struct
 
         val v = alpha 0
 
-        val (mainGoal, mhole) = makeGoal @@ ([(v, P.DIM)],[]) |> H >> CJ.TRUE (substSymbol (P.ret v, u) a)
+        val (mainGoal, mhole) = makeGoal @@ ([(v, P.DIM)],[]) || H >> CJ.TRUE (substSymbol (P.ret v, u) a)
 
         val m0 = mhole [(P.APP P.DIM0, P.DIM)] []
         val m1 = mhole [(P.APP P.DIM1, P.DIM)] []
-        val (cohGoal0, _) = makeGoal @@ H >> CJ.EQ ((m0, p0), a0)
-        val (cohGoal1, _) = makeGoal @@ H >> CJ.EQ ((m1, p1), a1)
+        val (cohGoal0, _) = makeGoal @@ ([],[]) || H >> CJ.EQ ((m0, p0), a0)
+        val (cohGoal1, _) = makeGoal @@ ([],[]) || H >> CJ.EQ ((m1, p1), a1)
 
         val psi = T.empty >: mainGoal >: cohGoal0 >: cohGoal1
         val abstr = Syn.into @@ Syn.ID_ABS (v, mhole [(P.ret v, P.DIM)] [])
@@ -664,9 +665,9 @@ struct
         val m00 = substSymbol (P.APP P.DIM0, v) m0v
         val m01 = substSymbol (P.APP P.DIM1, v) m0v
 
-        val (goalM, _) = makeGoal @@ ([(z, P.DIM)], []) |> H >> CJ.EQ ((m0z, m1z), az)
-        val (goalM00, _) = makeGoal @@ H >> CJ.EQ ((m00, p0), a0)
-        val (goalM01, _) = makeGoal @@ H >> CJ.EQ ((m01, p1), a1)
+        val (goalM, _) = makeGoal @@ ([(z, P.DIM)], []) || H >> CJ.EQ ((m0z, m1z), az)
+        val (goalM00, _) = makeGoal @@ ([],[]) || H >> CJ.EQ ((m00, p0), a0)
+        val (goalM01, _) = makeGoal @@ ([],[]) || H >> CJ.EQ ((m01, p1), a1)
       in
         T.empty >: goalM >: goalM00 >: goalM01
           #> trivial
@@ -679,10 +680,10 @@ struct
         val Syn.ID_AP (m0, r0) = Syn.out ap0
         val Syn.ID_AP (m1, r1) = Syn.out ap1
         val () = assertParamEq "Path.ApEq" (r0, r1)
-        val (goalSynth, holeSynth) = makeGoal @@ H >> CJ.SYNTH m0
-        val (goalMem, _) = makeGoal @@ H >> CJ.EQ ((m0, m1), holeSynth [] [])
-        val (goalLine, holeLine) = makeGoal @@ MATCH (O.MONO O.ID_TY, 0, holeSynth [] [])
-        val (goalTy, _) = makeGoal @@ H >> CJ.EQ_TYPE (ty, holeLine [(r0, P.DIM)] [])
+        val (goalSynth, holeSynth) = makeGoal @@ ([],[]) || H >> CJ.SYNTH m0
+        val (goalMem, _) = makeGoal @@ ([],[]) || H >> CJ.EQ ((m0, m1), holeSynth [] [])
+        val (goalLine, holeLine) = makeGoal @@ ([],[]) || MATCH (O.MONO O.ID_TY, 0, holeSynth [] [])
+        val (goalTy, _) = makeGoal @@ ([],[]) || H >> CJ.EQ_TYPE (ty, holeLine [(r0, P.DIM)] [])
       in
         T.empty >: goalSynth >: goalMem >: goalLine >: goalTy
           #> trivial
@@ -693,13 +694,13 @@ struct
         val _ = RedPrlLog.trace "Path.ApComputeConst"
         val H >> CJ.EQ ((ap, p), a) = jdg
         val Syn.ID_AP (m, P.APP r) = Syn.out ap
-        val (goalSynth, holeSynth) = makeGoal @@ H >> CJ.SYNTH m
+        val (goalSynth, holeSynth) = makeGoal @@ ([],[]) || H >> CJ.SYNTH m
 
         val dimAddr = case r of P.DIM0 => 1 | P.DIM1 => 2 | _ => raise Fail "impossible"
-        val (goalLine, holeLine) = makeGoal @@ MATCH (O.MONO O.ID_TY, 0, holeSynth [] [])
-        val (goalEndpoint, holeEndpoint) = makeGoal @@ MATCH (O.MONO O.ID_TY, dimAddr, holeSynth [] [])
-        val (goalTy, _) = makeGoal @@ H >> CJ.EQ_TYPE (a, holeLine [(P.APP r, P.DIM)] [])
-        val (goalEq, _) = makeGoal @@ H >> CJ.EQ ((holeEndpoint [] [], p), a)
+        val (goalLine, holeLine) = makeGoal @@ ([],[]) || MATCH (O.MONO O.ID_TY, 0, holeSynth [] [])
+        val (goalEndpoint, holeEndpoint) = makeGoal @@ ([],[]) || MATCH (O.MONO O.ID_TY, dimAddr, holeSynth [] [])
+        val (goalTy, _) = makeGoal @@ ([],[]) || H >> CJ.EQ_TYPE (a, holeLine [(P.APP r, P.DIM)] [])
+        val (goalEq, _) = makeGoal @@ ([],[]) || H >> CJ.EQ ((holeEndpoint [] [], p), a)
       in
         T.empty >: goalSynth >: goalLine >: goalEndpoint >: goalTy >: goalEq
           #> trivial
@@ -712,8 +713,8 @@ struct
         val Syn.ID_TY ((u, a), p0, p1) = Syn.out pathTy
 
         val m' = Syn.into @@ Syn.ID_ABS (u, Syn.into @@ Syn.ID_AP (m, P.ret u))
-        val (goal1, _) = makeGoal @@ H >> CJ.MEM (m, pathTy)
-        val (goal2, _) = makeGoal @@ H >> CJ.EQ ((m', n), pathTy)
+        val (goal1, _) = makeGoal @@ ([],[]) || H >> CJ.MEM (m, pathTy)
+        val (goal2, _) = makeGoal @@ ([],[]) || H >> CJ.EQ ((m', n), pathTy)
       in
         T.empty >: goal1 >: goal2
           #> trivial
@@ -721,81 +722,7 @@ struct
 
   end
 
-  structure Generic =
-  struct
-    fun splitList (xs, n) =
-      (List.take (xs, n), List.drop (xs, n))
-      handle _=> raise Fail "splitlist"
-
-    fun liftTelescope (U, G) psi =
-      let
-        val (us', sigmas') = ListPair.unzip U
-        val (xs', taus') = ListPair.unzip G
-
-        open T.ConsView
-        fun go EMPTY env psi' = psi'
-          | go (CONS (x, jdg, psi)) env psi' =
-              let
-                 val vl as ((psorts, vsorts), tau) = J.sort jdg
-                 val us = List.map (fn _ => Sym.named "u") psorts
-                 val xs = List.map (fn _ => Var.named "x") vsorts
-
-                 val ps = ListPair.map (fn (u, sigma) => (P.ret u, sigma)) (us' @ us, sigmas' @ psorts)
-                 val ms = ListPair.map (fn (x, tau) => check (`x, tau)) (xs' @ xs, taus' @ vsorts)
-
-                 val m = check (x $# (ps, ms), tau)
-                 val b = checkb ((us, xs) \ m, vl)
-
-                 val jdg' = (U, G) |> J.subst env jdg
-                 val env' = Metavar.Ctx.insert env x b
-              in
-                go (out psi) env' (T.snoc psi' x jdg')
-              end
-      in
-        go (out psi) Metavar.Ctx.empty T.empty
-      end
-
-    fun Lift tac alpha jdg =
-      let
-        val (U, G) |> jdg' = jdg
-
-        val st as Lcf.|> (psi, vld) = tac alpha jdg'
 
-        val psi' = liftTelescope (U, G) psi
-
-        val (us', sigmas') = ListPair.unzip U
-        val (xs', taus') = ListPair.unzip G
-
-        fun lower abs =
-          let
-            val ((us, xs) \ m, ((sigmas, taus), tau)) = inferb abs
-            val (us1, us2) = splitList (us, List.length U)
-            val (sigmas1, sigmas2) = splitList (sigmas, List.length U)
-            val (xs1, xs2) = splitList (xs, List.length G)
-            val (taus1, taus2) = splitList (taus, List.length G)
-
-            val srho = ListPair.foldl (fn (u1, (u', _), r) => Sym.Ctx.insert r u1 (P.ret u')) Sym.Ctx.empty (us1, U) handle _ => raise Fail "srho"
-            val xrho = ListPair.foldl (fn (x1, (x', taux), r) => Var.Ctx.insert r x1 (check (`x', taux))) Var.Ctx.empty (xs1, G) handle _ => raise Fail "xrho"
-            val m' = substVarenv xrho (substSymenv srho m)
-          in
-            checkb ((us2, xs2) \ m', ((sigmas2, taus2), tau))
-          end
-
-        fun lift abs =
-          let
-            val ((us, xs) \ m, ((sigmas, taus), tau)) = inferb abs
-          in
-            checkb ((us' @ us, xs' @ xs) \ m, ((sigmas' @ sigmas, taus' @ taus), tau))
-          end
-
-
-        (* No idea if what follows is correct, I'm just guessing at this point! *)
-        val env = T.foldl (fn (x, jdg, r) => Env.insert r x (lower (LcfLanguage.var x (J.sort jdg)))) Env.empty psi'
-        val vld' = lift @@ mapAbs (substMetaenv env) vld
-      in
-        Lcf.|> (psi', vld')
-      end
-  end
 
   structure Hyp =
   struct
@@ -820,7 +747,7 @@ struct
       let
         val _ = RedPrlLog.trace "Type.Intro"
         val H >> CJ.TYPE ty = jdg
-        val (goal, _) = makeGoal @@ H >> CJ.EQ_TYPE (ty, ty)
+        val (goal, _) = makeGoal @@ ([],[]) || H >> CJ.EQ_TYPE (ty, ty)
       in
         T.empty >: goal
           #> trivial
@@ -835,7 +762,7 @@ struct
     let
       val _ = RedPrlLog.trace "Equality.Symmetry"
       val H >> CJ.EQ_TYPE (ty1, ty2) = jdg
-      val (goal, hole) = makeGoal @@ H >> CJ.EQ_TYPE (ty2, ty1)
+      val (goal, hole) = makeGoal @@ ([],[]) || H >> CJ.EQ_TYPE (ty2, ty1)
     in
       T.empty >: goal
         #> trivial
@@ -848,7 +775,7 @@ struct
       let
         val _ = RedPrlLog.trace "True.Witness"
         val H >> CJ.TRUE ty = jdg
-        val (goal, _) = makeGoal @@ H >> CJ.MEM (tm, ty)
+        val (goal, _) = makeGoal @@ ([],[]) || H >> CJ.MEM (tm, ty)
       in
         T.empty >: goal
           #> tm
@@ -863,7 +790,7 @@ struct
       let
         val _ = RedPrlLog.trace "Membership.Intro"
         val H >> CJ.MEM (tm, ty) = jdg
-        val (goal, _) = makeGoal @@ H >> CJ.EQ ((tm, tm), ty)
+        val (goal, _) = makeGoal @@ ([],[]) || H >> CJ.EQ ((tm, tm), ty)
       in
         T.empty >: goal
           #> trivial
@@ -889,10 +816,10 @@ struct
         val _ = RedPrlLog.trace "Synth.Ap"
         val H >> CJ.SYNTH tm = jdg
         val Syn.AP (m, n) = Syn.out tm
-        val (goalDFun, holeDFun) = makeGoal @@ H >> CJ.SYNTH m
-        val (goalDom, holeDom) = makeGoal @@ MATCH (O.MONO O.DFUN, 0, holeDFun [] [])
-        val (goalCod, holeCod) = makeGoal @@ MATCH (O.MONO O.DFUN, 1, holeDFun [] [])
-        val (goalN, _) = makeGoal @@ H >> CJ.MEM (n, holeDom [] [])
+        val (goalDFun, holeDFun) = makeGoal @@ ([],[]) || H >> CJ.SYNTH m
+        val (goalDom, holeDom) = makeGoal @@ ([],[]) || MATCH (O.MONO O.DFUN, 0, holeDFun [] [])
+        val (goalCod, holeCod) = makeGoal @@ ([],[]) || MATCH (O.MONO O.DFUN, 1, holeDFun [] [])
+        val (goalN, _) = makeGoal @@ ([],[]) || H >> CJ.MEM (n, holeDom [] [])
       in
         T.empty >: goalDFun >: goalDom >: goalCod >: goalN
           #> holeCod [] [n]
@@ -905,7 +832,7 @@ struct
         val Syn.S1_ELIM ((x,cx), m, _) = Syn.out tm
 
         val cm = substVar (m, x) cx
-        val (goal, _) = makeGoal @@ H >> CJ.MEM (tm, cm)
+        val (goal, _) = makeGoal @@ ([],[]) || H >> CJ.MEM (tm, cm)
       in
         T.empty >: goal
           #> cm
@@ -918,7 +845,7 @@ struct
         val Syn.IF ((x,cx), m, _) = Syn.out tm
 
         val cm = substVar (m, x) cx
-        val (goal, _) = makeGoal @@ H >> CJ.MEM (tm, cm)
+        val (goal, _) = makeGoal @@ ([],[]) || H >> CJ.MEM (tm, cm)
       in
         T.empty >: goal
           #> cm
@@ -929,8 +856,8 @@ struct
         val _ = RedPrlLog.trace "Synth.PathAp"
         val H >> CJ.SYNTH tm = jdg
         val Syn.ID_AP (m, r) = Syn.out tm
-        val (goalPathTy, holePathTy) = makeGoal @@ H >> CJ.SYNTH m
-        val (goalLine, holeLine) = makeGoal @@ MATCH (O.MONO O.ID_TY, 0, holePathTy [] [])
+        val (goalPathTy, holePathTy) = makeGoal @@ ([],[]) || H >> CJ.SYNTH m
+        val (goalLine, holeLine) = makeGoal @@ ([],[]) || MATCH (O.MONO O.ID_TY, 0, holePathTy [] [])
         val psi = T.empty >: goalPathTy >: goalLine
       in
         T.empty >: goalPathTy >: goalLine
@@ -942,8 +869,8 @@ struct
         val _ = RedPrlLog.trace "Synth.Fst"
         val H >> CJ.SYNTH tm = jdg
         val Syn.FST m = Syn.out tm
-        val (goalTy, holeTy) = makeGoal @@ H >> CJ.SYNTH m
-        val (goalA, holeA) = makeGoal @@ MATCH (O.MONO O.DPROD, 0, holeTy [] [])
+        val (goalTy, holeTy) = makeGoal @@ ([],[]) || H >> CJ.SYNTH m
+        val (goalA, holeA) = makeGoal @@ ([],[]) || MATCH (O.MONO O.DPROD, 0, holeTy [] [])
       in
         T.empty >: goalTy >: goalA
           #> holeA [] []
@@ -954,8 +881,8 @@ struct
         val _ = RedPrlLog.trace "Synth.Snd"
         val H >> CJ.SYNTH tm = jdg
         val Syn.SND m = Syn.out tm
-        val (goalTy, holeTy) = makeGoal @@ H >> CJ.SYNTH m
-        val (goalB, holeB) = makeGoal @@ MATCH (O.MONO O.DPROD, 1, holeTy [] [])
+        val (goalTy, holeTy) = makeGoal @@ ([],[]) || H >> CJ.SYNTH m
+        val (goalB, holeB) = makeGoal @@ ([],[]) || MATCH (O.MONO O.DPROD, 1, holeTy [] [])
       in
         T.empty >: goalTy >: goalB
           #> holeB [] [Syn.into @@ Syn.FST m]
@@ -1008,7 +935,7 @@ struct
       let
         val _ = RedPrlLog.trace "Equality.Symmetry"
         val H >> CJ.EQ ((m, n), ty) = jdg
-        val (goal, hole) = makeGoal @@ H >> CJ.EQ ((n, m), ty)
+        val (goal, hole) = makeGoal @@ ([],[]) || H >> CJ.EQ ((n, m), ty)
       in
         T.empty >: goal
           #> trivial
@@ -1084,7 +1011,7 @@ struct
             val tube1 = substSymbol (P.ret w, v) tube1
             val J = H >> CJ.EQ ((tube0,tube1), ty)
           in
-            List.map (fn j => #1 (makeGoal (([(w, P.DIM)], []) |> j)))
+            List.map (fn j => #1 (makeGoal (([(w, P.DIM)], []) || j)))
                      (Restriction.Two J ext0 eps0 ext1 eps1)
           end
       in
@@ -1104,7 +1031,7 @@ struct
           let
             val J = H >> CJ.EQ ((substSymbol (r,u) tube, cap), ty)
           in
-            List.map (#1 o makeGoal) (Restriction.One J ext eps)
+            List.map (#1 o (fn j => makeGoal @@ ([],[]) || j)) (Restriction.One J ext eps)
           end
       in
         listToTel (ListMonad.bind tubeCap group)
@@ -1121,8 +1048,8 @@ struct
         val () = assertParamEq "HCom.Eq target of direction" (r'0, r'1)
         val _ = ListPair.mapEq (assertParamEq "HCom.Eq extents") (exts0, exts1)
 
-        val (goalTy, _) = makeGoal @@ H >> CJ.EQ_TYPE (ty0, ty1)
-        val (goalCap, _) = makeGoal @@ H >> CJ.EQ ((cap0, cap1), ty)
+        val (goalTy, _) = makeGoal @@ ([],[]) || H >> CJ.EQ_TYPE (ty0, ty1)
+        val (goalCap, _) = makeGoal @@ ([],[]) || H >> CJ.EQ ((cap0, cap1), ty)
 
         val w = alpha 0
 
@@ -1142,7 +1069,7 @@ struct
                 val tube1 = substSymbol (P.ret w, v) tube1
                 val J = H >> CJ.EQ ((tube0,tube1), ty)
               in
-                List.map (fn j => #1 (makeGoal (([(w, P.DIM)], []) |> j)))
+                List.map (fn j => #1 (makeGoal (([(w, P.DIM)], []) || j)))
                          (Restriction.One J ext eps)
               end
           in
@@ -1167,8 +1094,8 @@ struct
         val () = assertAlphaEq (ty0, ty)
         val group = groupTubes exts tubes
 
-        val (goalTy, _) = makeGoal @@ H >> CJ.TYPE ty
-        val (goalEq, _) = makeGoal @@ H >> CJ.EQ ((cap, rhs), ty)
+        val (goalTy, _) = makeGoal @@ ([],[]) || H >> CJ.TYPE ty
+        val (goalEq, _) = makeGoal @@ ([],[]) || H >> CJ.EQ ((cap, rhs), ty)
 
         val w = alpha 0
       in
@@ -1194,9 +1121,9 @@ struct
 
         val group = groupTubes exts tubes
 
-        val (goalTy, _) = makeGoal @@ H >> CJ.TYPE ty
-        val (goalCap, _) = makeGoal @@ H >> CJ.MEM (cap, ty)
-        val (goalEq, _) = makeGoal @@ H >> CJ.EQ ((substSymbol (r', u) tube, rhs), ty)
+        val (goalTy, _) = makeGoal @@ ([],[]) || H >> CJ.TYPE ty
+        val (goalCap, _) = makeGoal @@ ([],[]) || H >> CJ.MEM (cap, ty)
+        val (goalEq, _) = makeGoal @@ ([],[]) || H >> CJ.EQ ((substSymbol (r', u) tube, rhs), ty)
 
         val w = alpha 0
       in
@@ -1276,7 +1203,7 @@ struct
         val H >> CJ.EQ ((m, n), ty) = jdg
         val Abt.$ (theta, _) = Abt.out m
         val m' = Machine.unload sign (safeEval sign (Machine.load m))
-        val (goal, _) = makeGoal @@ H >> CJ.EQ ((m', n), ty)
+        val (goal, _) = makeGoal @@ ([],[]) || H >> CJ.EQ ((m', n), ty)
       in
         T.empty >: goal
           #> trivial
@@ -1288,7 +1215,7 @@ struct
         val H >> CJ.EQ_TYPE (ty1, ty2) = jdg
         val Abt.$ (theta, _) = Abt.out ty1
         val ty1' = Machine.unload sign (safeEval sign (Machine.load ty1))
-        val (goal, _) = makeGoal @@ H >> CJ.EQ_TYPE (ty1', ty2)
+        val (goal, _) = makeGoal @@ ([],[]) || H >> CJ.EQ_TYPE (ty1', ty2)
         in
           T.empty >: goal
             #> trivial
@@ -1301,8 +1228,8 @@ struct
       val H >> catjdg' = jdg
       val z = alpha 0
       val tau = CJ.synthesis catjdg
-      val (goal1, hole1) = makeGoal @@ ([], [(z, tau)]) |> H @> (z, catjdg) >> catjdg'
-      val (goal2, hole2) = makeGoal @@ H >> catjdg
+      val (goal1, hole1) = makeGoal @@ ([], [(z, tau)]) || H @> (z, catjdg) >> catjdg'
+      val (goal2, hole2) = makeGoal @@ ([],[]) || H >> catjdg
     in
       T.empty >: goal1 >: goal2
         #> hole1 [] [hole2 [] []]
@@ -1319,11 +1246,6 @@ struct
       T.empty #> evd
     end
 
-  fun Lift tac alpha jdg =
-    case jdg of
-       _ |> _ => Generic.Lift (Lift tac) alpha jdg
-     | _ => tac alpha jdg
-
   local
     fun matchGoal f alpha jdg =
       f jdg alpha jdg
diff --git a/src/redprl/refiner.sig b/src/redprl/refiner.sig
index ba85f3077..bdc935976 100644
--- a/src/redprl/refiner.sig
+++ b/src/redprl/refiner.sig
@@ -6,7 +6,6 @@ sig
   type rule
   type hyp
 
-  val Lift : rule -> rule
   val Lemma : abt -> 'n -> Lcf.jdg Lcf.tactic
   val Cut : catjdg -> rule
   val Elim : sign -> hyp -> rule
diff --git a/src/redprl/refiner_kit.fun b/src/redprl/refiner_kit.fun
index 66e6bcbda..27c775586 100644
--- a/src/redprl/refiner_kit.fun
+++ b/src/redprl/refiner_kit.fun
@@ -1,36 +1,64 @@
 structure LcfLanguage = LcfAbtLanguage (RedPrlAbt)
 
+signature LCF_GENERIC_UTIL = 
+sig
+  structure Abt : ABT
+  datatype 'a generic = || of ((Abt.symbol * Abt.psort) list * (Abt.variable * Abt.sort) list) * 'a
+  include LCF_UTIL where type 'a Eff.t = 'a generic
+end
+
 structure Lcf :
 sig
-  include LCF_UTIL
+  include LCF_GENERIC_UTIL
   val prettyState : jdg state -> PP.doc
   val stateToString : jdg state -> string
 end =
 struct
-  structure Def = LcfUtil (structure Lcf = Lcf (LcfLanguage) and J = RedPrlJudgment)
-  open Def
-  infix |>
-
-  fun prettyGoal (x, jdg) =
-    PP.concat
-      [PP.text "Goal ",
-       PP.text (RedPrlAbt.Metavar.toString x),
-       PP.text ".",
-       PP.nest 2 (PP.concat [PP.line, RedPrlSequent.pretty TermPrinter.toString jdg]),
-       PP.line]
-
-  val prettyGoals : jdg Tl.telescope -> {doc : PP.doc, env : J.env, idx : int} =
+  structure LcfGeneric = LcfGeneric (LcfLanguage)
+  structure Def = LcfGenericUtil (structure Lcf = LcfGeneric and J = RedPrlJudgment)
+  open Def LcfGeneric
+  infix |> ||
+
+
+  val prettySyms =
+    PP.text o ListSpine.pretty (fn (u, sigma) => Sym.toString u ^ " : " ^ Abt.O.Ar.Vl.PS.toString sigma) ", "
+
+  val prettyVars = 
+    PP.text o ListSpine.pretty (fn (x, tau) => Var.toString x ^ " : " ^ Abt.O.Ar.Vl.S.toString tau) ", "
+
+  fun prettyGoal (syms, vars) (x, jdg) =
+    let
+      val parametric = 
+        if List.length syms > 0 then
+          PP.concat [PP.line, PP.text "nabla {", prettySyms syms, PP.text "}. "]
+        else
+          PP.empty
+    in
+      PP.concat
+        [PP.text "Goal ",
+         PP.text (RedPrlAbt.Metavar.toString x),
+         PP.text ".",
+         parametric,
+         PP.nest 2 (PP.concat [PP.line, RedPrlSequent.pretty TermPrinter.toString jdg]),
+         PP.line]
+    end
+
+
+  val prettyGoals : jdg eff Tl.telescope -> {doc : PP.doc, env : J.env, idx : int} =
     let
       open RedPrlAbt
     in
       Tl.foldl
-        (fn (x, jdg, {doc, env, idx}) =>
+        (fn (x, (syms, vars) || jdg, {doc, env, idx}) =>
           let
             val x' = Metavar.named (Int.toString idx)
             val jdg' = J.subst env jdg
-            val env' = Metavar.Ctx.insert env x (LcfLanguage.var x' (J.sort jdg'))
+            val ((ssorts, vsorts), tau) = J.sort jdg'
+            val vl' = ((ssorts @ List.map #2 syms, vsorts @ List.map #2 vars), tau)
+            val env' = Metavar.Ctx.insert env x (LcfLanguage.var x' vl')
+
           in
-            {doc = PP.concat [doc, prettyGoal (x', jdg'), PP.line],
+            {doc = PP.concat [doc, prettyGoal (syms, vars) (x', jdg'), PP.line],
              env = env',
              idx = idx + 1}
           end)
@@ -97,14 +125,14 @@ struct
       end
   end
 
-  fun makeGoal jdg =
+  fun makeGoal (Lcf.|| (bs, jdg)) =
     let
       open Abt infix 1 $#
       val x = newMeta ""
       val vl as (_, tau) = J.sort jdg
-      fun hole ps ms = check (x $# (ps, ms), tau)
+      fun hole ps ms = check (x $# (ps, ms), tau) handle _ => raise Fail "makeGoal"
     in
-      ((x, jdg), hole)
+      ((x, Lcf.|| (bs, jdg)), hole)
     end
 
 
diff --git a/src/redprl/sequent.sig b/src/redprl/sequent.sig
index 425f969e6..491c77ee0 100644
--- a/src/redprl/sequent.sig
+++ b/src/redprl/sequent.sig
@@ -15,7 +15,6 @@ sig
 
   datatype 'a jdg =
      >> of 'a CJ.jdg ctx * 'a CJ.jdg                            (* sequents / formal hypothetical judgment *)
-   | |> of ((sym * psort) list * (var * sort) list) * 'a jdg    (* generic+parametric judgment *)
    | MATCH of operator * int * 'a                               (* unify a term w/ a head operator and extract the kth subterm *)
 
   val map : ('a -> 'b) -> 'a jdg -> 'b jdg
diff --git a/src/redprl/sequent.sml b/src/redprl/sequent.sml
index c29f95f0d..0145c0b64 100644
--- a/src/redprl/sequent.sml
+++ b/src/redprl/sequent.sml
@@ -15,14 +15,12 @@ struct
 
   datatype 'a jdg =
      >> of 'a CJ.jdg ctx * 'a CJ.jdg
-   | |> of ((sym * psort) list * (var * sort) list) * 'a jdg
    | MATCH of operator * int * 'a
 
-  infix >> |>
+  infix >>
 
   fun map f =
     fn H >> catjdg => Hyps.map (CJ.map f) H >> CJ.map f catjdg
-     | (U,G) |> jdg => (U,G) |> map f jdg
      | MATCH (th, k, a) => MATCH (th, k, f a)
 
   local
@@ -43,10 +41,6 @@ struct
     fn (H1 >> catjdg1, H2 >> catjdg2) =>
           telescopeEq (H1, H2)
             andalso CJ.eq (catjdg1, catjdg2)
-     | ((U1,G1) |> jdg1, (U2,G2) |> jdg2) =>
-          ListPair.allEq (fn ((u1, sort1), (u2, sort2)) => CJ.Tm.Sym.eq (u1, u2) andalso CJ.Tm.O.Ar.Vl.PS.eq (sort1, sort2)) (U1, U2)
-            andalso ListPair.allEq (fn ((x1, sort1), (x2, sort2)) => CJ.Tm.Var.eq (x1, x2) andalso CJ.Tm.O.Ar.Vl.S.eq (sort1, sort2)) (G1, G2)
-            andalso eq (jdg1, jdg2)
      | (MATCH (th1, k1, a1), MATCH (th2, k2, a2)) =>
           CJ.Tm.O.eq CJ.Tm.Sym.eq (th1, th2)
             andalso k1 = k2
@@ -64,7 +58,6 @@ struct
     fun pretty f : 'a jdg -> doc =
       fn H >> catjdg => concat [prettyHyps (CJ.pretty f) H, text "\226\138\162 ", CJ.pretty f catjdg]
        | MATCH (th, k, a) => concat [text (f a), text " match ", text (Tm.O.toString Tm.Sym.toString th), text " @ ", int k]
-       | (U, G) |> jdg => pretty f jdg
   end
 
   fun toString f = PP.toString 80 true o pretty f
diff --git a/test/success/bool-hcom.prl b/test/success/bool-hcom.prl
index 7070fab29..1acf62486 100644
--- a/test/success/bool-hcom.prl
+++ b/test/success/bool-hcom.prl
@@ -8,7 +8,8 @@ Thm BasicHcom : [
   { lam a. lam b. lam c. lam d.
     lam pab. lam pac. lam pbd.
     <i> 'hcom{i; 0 ~> 1}(bool; ,pab @ i; {j}. ,pac @ j; {j}. ,pbd @ j)
-  }; auto
+  };
+  <|auto|>;
 ].
 
 Thm Cap{i : dim} : [ hcom{i; 0 ~> 0}(bool; tt; {_}. tt; {_}. tt) = tt : bool ] by [