diff --git a/src/core/Conversion.ml b/src/core/Conversion.ml
index f674decca..53147ce73 100644
--- a/src/core/Conversion.ml
+++ b/src/core/Conversion.ml
@@ -106,8 +106,12 @@ let rec equate_tp (tp0 : D.tp) (tp1 : D.tp) =
   | D.Circle, D.Circle
   | D.Univ, D.Univ ->
     ret ()
-  | D.ElStable code0, D.ElStable code1 ->
-    equate_stable_code D.Univ code0 code1
+  | D.ElStable code0, _ ->
+    let* tp0 = lift_cmp @@ Sem.unfold_el code0 in
+    equate_tp tp0 tp1
+  | _, D.ElStable code1 ->
+    let* tp1 = lift_cmp @@ Sem.unfold_el code1 in
+    equate_tp tp0 tp1
   | D.ElCut cut0, D.ElCut cut1 ->
     equate_cut cut0 cut1
   | D.ElUnstable (`HCom (r0, s0, phi0, bdy0)), D.ElUnstable (`HCom (r1, s1, phi1, bdy1)) ->
@@ -232,10 +236,8 @@ and equate_con tp con0 con1 =
     let* out1 = lift_cmp @@ do_sub_out con1 in
     equate_con tp out0 out1
   | D.ElStable code, _, _ ->
-    let* out0 = lift_cmp @@ do_el_out con0 in
-    let* out1 = lift_cmp @@ do_el_out con1 in
     let* tp = lift_cmp @@ unfold_el code in
-    equate_con tp out0 out1
+    equate_con tp con0 con1
   | _, D.Zero, D.Zero ->
     ret ()
   | _, D.Suc con0, D.Suc con1 ->
@@ -260,7 +262,7 @@ and equate_con tp con0 con1 =
       Splice.con bdy @@ fun bdy ->
       Splice.term @@
       TB.lam @@ fun i -> TB.lam @@ fun prf ->
-      TB.el_in @@ TB.ap bdy [i; prf]
+      TB.ap bdy [i; prf]
     in
     let* bdy0' = fix_body bdy0 in
     let* bdy1' = fix_body bdy1 in
@@ -271,7 +273,7 @@ and equate_con tp con0 con1 =
       Splice.con bdy @@ fun bdy ->
       Splice.term @@
       TB.lam @@ fun i -> TB.lam @@ fun prf ->
-      TB.el_in @@ TB.ap bdy [i; prf]
+      TB.ap bdy [i; prf]
     in
     let* bdy0' = fix_body bdy0 in
     let* bdy1' = fix_body bdy1 in
@@ -401,8 +403,6 @@ and equate_frm k0 k1 =
       TB.el @@ TB.ap mot [TB.loop x]
     in
     equate_con loop_tp loop_case0 loop_case1
-  | D.KElOut, D.KElOut ->
-    ret ()
   | _ ->
     conv_err @@ ExpectedFrmEq (k0, k1)
 
diff --git a/src/core/Domain.ml b/src/core/Domain.ml
index afa64b698..ca4dc1b68 100644
--- a/src/core/Domain.ml
+++ b/src/core/Domain.ml
@@ -33,8 +33,6 @@ struct
   let snd = Lam (`Anon, Clo (S.Snd (S.Var 0), {tpenv = Emp; conenv = Emp}))
 
   let proj lbl = Lam (`Anon, Clo (S.Proj (S.Var 0, lbl), {tpenv = Emp; conenv = Emp}))
-  let el_out = Lam (`Anon, Clo (S.ElOut (S.Var 0), {tpenv = Emp; conenv = Emp}))
-
   let tm_abort = Split []
   let tp_abort = TpSplit []
 
@@ -106,7 +104,6 @@ struct
     | KProj lbl -> Format.fprintf fmt "proj[%a]" Ident.pp_user lbl
     | KNatElim _ -> Format.fprintf fmt "<nat-elim>"
     | KCircleElim _ -> Format.fprintf fmt "<circle-elim>"
-    | KElOut -> Uuseg_string.pp_utf_8 fmt "⭝ₑₗ"
 
   and pp_cof : cof Pp.printer =
     fun fmt cof ->
@@ -174,8 +171,6 @@ struct
       Format.fprintf fmt "dim0"
     | Dim1 ->
       Format.fprintf fmt "dim1"
-    | ElIn con ->
-      Format.fprintf fmt "el/in[%a]" pp_con con
     | StableCode `Nat ->
       Format.fprintf fmt "nat/code"
     | StableCode `Circle ->
diff --git a/src/core/Domain.mli b/src/core/Domain.mli
index ea53d28e0..e0a781ba8 100644
--- a/src/core/Domain.mli
+++ b/src/core/Domain.mli
@@ -23,7 +23,6 @@ module Make : functor (Symbol : Symbol.S) -> sig
   val fst : con
   val snd : con
   val proj : Ident.user -> con
-  val el_out : con
 
   val tm_abort : con
   val tp_abort : tp
diff --git a/src/core/DomainData.ml b/src/core/DomainData.ml
index b028bdf41..cd9965646 100644
--- a/src/core/DomainData.ml
+++ b/src/core/DomainData.ml
@@ -70,10 +70,7 @@ struct
     | Pair of con * con
     | Struct of (Ident.user * con) list
     | SubIn of con
-
-    | ElIn of con
-    (** The introduction form for the extension of a {i stable} type code only (see {!constructor:ElStable} and {!constructor:ElUnstable}). *)
-
+    
     | Dim0
     | Dim1
     | DimProbe of DimProbe.t
@@ -139,10 +136,6 @@ struct
     | KNatElim of con * con * con
     | KCircleElim of con * con * con
 
-    | KElOut
-    (** The elimination form for the extension of a {i stable} type code only (see {!constructor:ElStable}). *)
-
-
   (** An {i unstable} frame is a {i dimension substitution-unstable} elimination form with a hole in place of its principal argument. *)
   and unstable_frm =
     | KHCom of dim * dim * cof * con
diff --git a/src/core/Quote.ml b/src/core/Quote.ml
index 0902c7c92..531360af5 100644
--- a/src/core/Quote.ml
+++ b/src/core/Quote.ml
@@ -115,12 +115,8 @@ let rec quote_con (tp : D.tp) con =
     S.SubIn tout
 
   | D.ElStable code, _ ->
-    let+ tout =
-      let* unfolded = lift_cmp @@ unfold_el code in
-      let* out = lift_cmp @@ do_el_out con in
-      quote_con unfolded out
-    in
-    S.ElIn tout
+    let* unfolded = lift_cmp @@ unfold_el code in
+    quote_con unfolded con
 
   | _, D.Zero ->
     ret S.Zero
@@ -160,10 +156,9 @@ let rec quote_con (tp : D.tp) con =
       Splice.con bdy @@ fun bdy ->
       Splice.term @@
       TB.lam @@ fun i -> TB.lam @@ fun prf ->
-      TB.el_in @@ TB.ap bdy [i; prf]
+      TB.ap bdy [i; prf]
     in
-    let+ tm = quote_hcom (D.StableCode `Nat) r s phi bdy' in
-    S.ElOut tm
+    quote_hcom (D.StableCode `Nat) r s phi bdy'
 
   | _univ, D.UnstableCode (`V (r, pcode, code, pequiv)) ->
     let+ tr, t_pcode, tcode, t_pequiv = quote_v_data r pcode code pequiv in
@@ -176,10 +171,9 @@ let rec quote_con (tp : D.tp) con =
       Splice.con bdy @@ fun bdy ->
       Splice.term @@
       TB.lam @@ fun i -> TB.lam @@ fun prf ->
-      TB.el_in @@ TB.ap bdy [i; prf]
+      TB.ap bdy [i; prf]
     in
-    let+ tm = quote_hcom (D.StableCode `Univ) r s phi bdy' in
-    S.ElOut tm
+    quote_hcom (D.StableCode `Univ) r s phi bdy'
 
   | D.Circle, D.FHCom (`Circle, r, s, phi, bdy) ->
     let* bdy' =
@@ -187,10 +181,9 @@ let rec quote_con (tp : D.tp) con =
       Splice.con bdy @@ fun bdy ->
       Splice.term @@
       TB.lam @@ fun i -> TB.lam @@ fun prf ->
-      TB.el_in @@ TB.ap bdy [i; prf]
+      TB.ap bdy [i; prf]
     in
-    let+ tm = quote_hcom (D.StableCode `Circle) r s phi bdy' in
-    S.ElOut tm
+    quote_hcom (D.StableCode `Circle) r s phi bdy'
 
   | D.ElUnstable (`HCom (r,s,phi,bdy)), _ ->
     let+ tr = quote_dim r
@@ -650,5 +643,3 @@ and quote_frm tm =
   | D.KAp (tp, con) ->
     let+ targ = quote_con tp con in
     S.Ap (tm, targ)
-  | D.KElOut ->
-    ret @@ S.ElOut tm
diff --git a/src/core/Refiner.ml b/src/core/Refiner.ml
index 6dc3070e3..6b83c5eef 100644
--- a/src/core/Refiner.ml
+++ b/src/core/Refiner.ml
@@ -653,7 +653,7 @@ struct
               Splice.con vpatch @@ fun patch ->
               Splice.term @@ TB.lams (field_names :> Ident.t list) @@ fun args -> TB.code_ext 0 (TB.ap field_tp @@ ListUtil.zip_with (@@) elim_conns args) TB.top @@ TB.lam @@ fun _ -> TB.ap patch args
             in
-            (ext_code, fun arg -> TB.sub_out @@ TB.el_out arg)
+            (ext_code, TB.sub_out)
           | None ->
             let+ code =
               RM.lift_cmp @@
@@ -697,7 +697,7 @@ struct
       RM.lift_cmp @@
       Sem.splice_tm @@
       Splice.con vtm @@ fun tm ->
-      Splice.term @@ TB.lams (sign_names :> Ident.t list) @@ fun args -> TB.el_out @@ TB.ap tm [TB.el_in @@ TB.struct_ @@ List.combine sign_names args]
+      Splice.term @@ TB.lams (sign_names :> Ident.t list) @@ fun args -> TB.ap tm [TB.struct_ @@ List.combine sign_names args]
     in
     let+ qfib = RM.quote_con fib_tp fib in
     S.CodeSignature (qsign @ [`User ["fib"], qfib])
@@ -745,7 +745,7 @@ struct
         TB.ap bdry [TB.prf]
       in
       let+ ttm = RM.lift_qu @@ Qu.quote_con tp tm in
-      S.ElIn (S.SubIn ttm)
+      S.SubIn ttm
     | tp -> RM.expected_connective `ElExt tp
 
   let code_v (tac_dim : T.Chk.tac) (tac_pcode: T.Chk.tac) (tac_code : T.Chk.tac) (tac_pequiv : T.Chk.tac) : T.Chk.tac =
@@ -936,14 +936,14 @@ struct
   let intro tac =
     T.Chk.brule ~name:"El.intro" @@ fun (tp, phi, clo) ->
     let* unfolded = dest_el tp in
-    let+ tm = T.Chk.brun tac (unfolded, phi, D.un_lam @@ D.compose D.el_out @@ D.Lam (`Anon, clo)) in
-    S.ElIn tm
+    T.Chk.brun tac (unfolded, phi, D.un_lam @@ D.Lam (`Anon, clo))
 
   let elim tac =
     T.Syn.rule ~name:"El.elim" @@
     let* tm, tp = T.Syn.run tac in
     let+ unfolded = dest_el tp in
-    S.ElOut tm, unfolded
+    tm, unfolded
+
 end
 
 
@@ -1214,7 +1214,7 @@ struct
 
   let assert_nat =
     function
-    | D.Nat -> RM.ret ()
+    | D.Nat | D.ElStable `Nat -> RM.ret ()
     | tp -> RM.expected_connective `Nat tp
 
   let rec int_to_term =
@@ -1282,7 +1282,7 @@ struct
 
   let assert_circle =
     function
-    | D.Circle -> RM.ret ()
+    | D.Circle | D.ElStable `Circle -> RM.ret ()
     | tp -> RM.expected_connective `Circle tp
 
   let base =
diff --git a/src/core/Semantics.ml b/src/core/Semantics.ml
index af59fbc6f..45809bf7d 100644
--- a/src/core/Semantics.ml
+++ b/src/core/Semantics.ml
@@ -122,9 +122,6 @@ and push_subst_con : D.dim -> DimProbe.t -> D.con -> D.con CM.m =
   | D.StableCode code ->
     let+ code = subst_stable_code r x code in
     D.StableCode code
-  | D.ElIn con ->
-    let+ con = subst_con r x con in
-    D.ElIn con
   | D.SubIn con ->
     let+ con = subst_con r x con in
     D.SubIn con
@@ -375,7 +372,7 @@ and subst_frm : D.dim -> DimProbe.t -> D.frm -> D.frm CM.m =
   fun r x ->
   let open CM in
   function
-  | D.KFst | D.KSnd | D.KElOut | D.KProj _ as frm -> ret frm
+  | D.KFst | D.KSnd | D.KProj _ as frm -> ret frm
   | D.KAp (tp, arg) ->
     let+ tp = subst_tp r x tp
     and+ arg = subst_con r x arg in
@@ -564,12 +561,6 @@ and eval : S.t -> D.con EvM.m =
     | S.SubIn tm ->
       let+ con = eval tm in
       D.SubIn con
-    | S.ElOut tm ->
-      let* con = eval tm in
-      lift_cmp @@ do_el_out con
-    | S.ElIn tm ->
-      let+ con = eval tm in
-      D.ElIn con
     | S.Dim0 -> ret D.Dim0
     | S.Dim1 -> ret D.Dim1
     | S.Cof cof_f ->
@@ -726,7 +717,7 @@ and eval_cof tphi =
 and whnf_con ~style : D.con -> D.con whnf CM.m =
   let open CM in
   function
-  | D.Lam _ | D.BindSym _ | D.Zero | D.Suc _ | D.Base | D.Pair _ | D.Struct _ | D.SubIn _ | D.ElIn _ | D.LockedPrfIn _
+  | D.Lam _ | D.BindSym _ | D.Zero | D.Suc _ | D.Base | D.Pair _ | D.Struct _ | D.SubIn _ | D.LockedPrfIn _
   | D.Cof _ | D.Dim0 | D.Dim1 | D.Prf | D.StableCode _ | D.DimProbe _ ->
     ret `Done
   | D.LetSym (r, x, con) ->
@@ -941,11 +932,10 @@ and do_nat_elim (mot : D.con) zero (suc : D.con) : D.con -> D.con CM.m =
       let fam =
         TB.lam @@ fun i ->
         let fhcom =
-          TB.el_out @@
           TB.hcom TB.code_nat r i phi @@
           TB.lam @@ fun j ->
           TB.lam @@ fun prf ->
-          TB.el_in @@ TB.ap bdy [j; prf]
+          TB.ap bdy [j; prf]
         in
         TB.ap mot [fhcom]
       in
@@ -997,11 +987,10 @@ and do_circle_elim (mot : D.con) base (loop : D.con) c : D.con CM.m =
     let fam =
       TB.lam @@ fun i ->
       let fhcom =
-        TB.el_out @@
         TB.hcom TB.code_circle r i phi @@
         TB.lam @@ fun j ->
         TB.lam @@ fun prf ->
-        TB.el_in @@ TB.ap bdy [j; prf]
+        TB.ap bdy [j; prf]
       in
       TB.ap mot [fhcom]
     in
@@ -1079,6 +1068,9 @@ and do_fst con : D.con CM.m =
       splitter con @@ List.map fst branches
     | D.Cut {tp = D.Sg (base, _, _); cut} ->
       ret @@ cut_frm ~tp:base ~cut D.KFst
+    | D.Cut {tp = D.ElStable (`Sg _ as code) ; cut} ->
+      let* tp = unfold_el code in
+      do_fst (D.Cut {tp ; cut})
     | _ ->
       throw @@ NbeFailed "Couldn't fst argument in do_fst"
   end
@@ -1100,6 +1092,9 @@ and do_snd con : D.con CM.m =
       let* fst = do_fst con in
       let+ fib = inst_tp_clo fam fst in
       cut_frm ~tp:fib ~cut D.KSnd
+    | D.Cut {tp = D.ElStable (`Sg _ as code) ; cut} ->
+      let* tp = unfold_el code in
+      do_snd (D.Cut {tp ; cut})
     | _ ->
       throw @@ NbeFailed ("Couldn't snd argument in do_snd")
   end
@@ -1135,6 +1130,9 @@ and do_proj (con : D.con) (lbl : Ident.user) : D.con CM.m =
       splitter con @@ List.map fst branches
     | D.Cut {tp = D.Signature sign; cut} ->
       cut_frm_sign cut sign lbl
+    | D.Cut {tp = D.ElStable (`Signature _ as code); cut} ->
+      let* tp = unfold_el code in
+      do_proj (D.Cut {tp ; cut}) lbl
     | _ ->
       throw @@ NbeFailed ("Couldn't proj argument in do_proj")
   end
@@ -1176,7 +1174,9 @@ and do_ap con arg =
     | D.Cut {tp = D.Pi (base, _, fam); cut} ->
       let+ fib = inst_tp_clo fam arg in
       cut_frm ~tp:fib ~cut @@ D.KAp (base, arg)
-
+    | D.Cut {tp = D.ElStable ((`Pi _ | `Ext _) as code); cut} ->
+      let* tp = unfold_el code in
+      do_ap (D.Cut {tp ; cut}) arg
     | D.Cut {tp = D.TpSplit branches; _} as con ->
       splitter con @@ List.map fst branches
 
@@ -1202,6 +1202,9 @@ and do_sub_out con =
       ret con
     | D.Cut {tp = D.Sub (tp, phi, clo); cut} ->
       ret @@ D.Cut {tp; cut = D.UnstableCut (cut, D.KSubOut (phi, clo)), []}
+    | D.Cut {tp = D.ElStable (`Ext (0,_,_,_) as code) ; cut} ->
+      let* tp = unfold_el code in
+      do_sub_out (D.Cut {tp ; cut})
     | D.Split branches as con ->
       splitter con @@ List.map fst branches
     | D.Cut {tp = D.TpSplit branches; _} as con ->
@@ -1294,34 +1297,6 @@ and do_rigid_vproj r pcode code pequiv v =
       throw @@ NbeFailed "do_rigid_vproj"
   end
 
-and do_el_out con =
-  let open CM in
-  abort_if_inconsistent (ret D.tm_abort) @@
-  let splitter con phis =
-    splice_tm @@
-    Splice.con con @@ fun tm ->
-    Splice.cons (List.map D.cof_to_con phis) @@ fun phis ->
-    Splice.term @@
-    TB.cof_split @@ List.map (fun phi -> phi, TB.el_out tm) phis
-  in
-  begin
-    inspect_con ~style:`UnfoldNone con |>>
-    function
-    | D.ElIn con ->
-      ret con
-    | D.Split branches as con ->
-      splitter con @@ List.map fst branches
-    | D.Cut {tp = D.TpSplit branches; _} as con ->
-      splitter con @@ List.map fst branches
-    | D.Cut {tp = D.ElStable code; cut} ->
-      let+ tp = unfold_el code in
-      cut_frm ~tp ~cut D.KElOut
-    | _ ->
-      Format.eprintf "bad el/out: %a@." D.pp_con con;
-      throw @@ NbeFailed "do_el_out"
-  end
-
-
 and do_el : D.con -> D.tp CM.m =
   let open CM in
   fun con ->
@@ -1342,7 +1317,7 @@ and do_el : D.con -> D.tp CM.m =
         splitter con @@ List.map fst branches
       | D.Cut {tp = D.TpSplit branches; _} as con ->
         splitter con @@ List.map fst branches
-      | D.Cut {cut; tp = D.Univ} ->
+      | D.Cut {cut; tp = D.Univ | D.ElStable `Univ} ->
         ret @@ D.ElCut cut
       | D.StableCode code ->
         ret @@ D.ElStable code
@@ -1586,18 +1561,18 @@ and enact_rigid_hcom code r r' phi bdy tag =
           Splice.con bdy @@ fun bdy ->
           Splice.term @@
           TB.lam @@ fun i -> TB.lam @@ fun prf ->
-          TB.el_out @@ TB.ap bdy [i; prf]
+          TB.ap bdy [i; prf]
         in
-        D.ElIn (D.FHCom (tag, r, r', phi, bdy'))
+        D.FHCom (tag, r, r', phi, bdy')
       | `Univ ->
         let+ bdy' =
           splice_tm @@
           Splice.con bdy @@ fun bdy ->
           Splice.term @@
           TB.lam @@ fun i -> TB.lam @@ fun prf ->
-          TB.el_out @@ TB.ap bdy [i; prf]
+          TB.ap bdy [i; prf]
         in
-        D.ElIn (D.UnstableCode (`HCom (r, r', phi, bdy')))
+        D.UnstableCode (`HCom (r, r', phi, bdy'))
     end
   | `Unstable code ->
     begin
@@ -1698,7 +1673,6 @@ and do_frm con =
   | D.KProj lbl -> do_proj con lbl
   | D.KNatElim (mot, case_zero, case_suc) -> do_nat_elim mot case_zero case_suc con
   | D.KCircleElim (mot, case_base, case_loop) -> do_circle_elim mot case_base case_loop con
-  | D.KElOut -> do_el_out con
 
 and do_spine con =
   let open CM in
diff --git a/src/core/Semantics.mli b/src/core/Semantics.mli
index 23a719ab3..9901925de 100644
--- a/src/core/Semantics.mli
+++ b/src/core/Semantics.mli
@@ -31,7 +31,6 @@ val do_fst : D.con -> D.con compute
 val do_snd : D.con -> D.con compute
 val do_proj : D.con -> Ident.user -> D.con compute
 val do_sub_out : D.con -> D.con compute
-val do_el_out : D.con -> D.con compute
 val unfold_el : D.con D.stable_code -> D.tp compute
 val do_el : D.con -> D.tp compute
 val do_spine : D.con -> D.frm list -> D.con compute
diff --git a/src/core/Serialize.ml b/src/core/Serialize.ml
index 1c6c3b0ea..5cc3cdcd3 100644
--- a/src/core/Serialize.ml
+++ b/src/core/Serialize.ml
@@ -137,8 +137,6 @@ struct
     | S.ForallCof cof -> labeled "forall" [json_of_tm cof]
     | S.CofSplit branches -> labeled "split" @@ List.map (fun (tphi, tm) -> json_of_pair (json_of_tm tphi) (json_of_tm tm)) branches
     | S.Prf -> `String "prf"
-    | S.ElIn tm -> labeled "el_in" [json_of_tm tm]
-    | S.ElOut tm -> labeled "el_out" [json_of_tm tm]
     | S.Box (r, s, phi, sides, cap) -> labeled "box" [json_of_tm r; json_of_tm s; json_of_tm phi; json_of_tm sides; json_of_tm cap]
     | S.Cap (r, s, phi, code, box) -> labeled "cap" [json_of_tm r; json_of_tm s; json_of_tm phi; json_of_tm code; json_of_tm box]
     | S.VIn (r, pequiv, pivot, base) -> labeled "v_in" [json_of_tm r; json_of_tm pequiv; json_of_tm pivot; json_of_tm base]
@@ -285,12 +283,6 @@ struct
       let branches = List.map (json_to_pair json_to_tm json_to_tm) j_branches in
       S.CofSplit branches
     | `String "prf" -> S.Prf
-    | `A [`String "el_in"; j_tm] ->
-      let tm = json_to_tm j_tm in
-      S.ElIn tm
-    | `A [`String "el_out"; j_tm] ->
-      let tm = json_to_tm j_tm in
-      S.ElOut tm
     | `A [`String "box"; j_r; j_s; j_phi; j_sides; j_cap] ->
       let r = json_to_tm j_r in
       let s = json_to_tm j_s in
@@ -445,7 +437,6 @@ struct
     | Pair (con0, con1) -> labeled "pair" [json_of_con con0; json_of_con con1]
     | Struct fields -> labeled "struct" [json_of_labeled json_of_con fields]
     | SubIn con -> labeled "sub_in" [json_of_con con]
-    | ElIn con -> labeled "el_in" [json_of_con con]
     | Dim0 -> `String "dim0"
     | Dim1 -> `String "dim1"
     | DimProbe dim_probe -> labeled "dim_probe" [DimProbe.serialize dim_probe]
@@ -522,7 +513,6 @@ struct
     | D.KProj lbl -> labeled "k_proj" [json_of_user lbl]
     | D.KNatElim (mot, z, s) -> labeled "k_nat_elim" [json_of_con mot; json_of_con z; json_of_con s]
     | D.KCircleElim (mot, b, l) -> labeled "k_circle_elim" [json_of_con mot; json_of_con b; json_of_con l]
-    | D.KElOut -> `String "k_el_out"
 
   and json_of_unstable_frm : D.unstable_frm -> J.value =
     function
@@ -568,7 +558,6 @@ struct
     | `A [`String "pair"; j_con0; j_con1] -> Pair (json_to_con j_con0, json_to_con j_con1)
     | `A [`String "struct"; j_fields] -> Struct (json_to_labeled json_to_con j_fields)
     | `A [`String "sub_in"; j_con] -> SubIn (json_to_con j_con)
-    | `A [`String "el_in"; j_con] -> ElIn (json_to_con j_con)
     | `String "dim0" -> Dim0
     | `String "dim1" -> Dim1
     | `A [`String "dim_probe"; j_dim_probe] -> DimProbe (DimProbe.deserialize j_dim_probe)
@@ -656,7 +645,6 @@ struct
     | `A [`String "k_proj"; j_lbl] -> KProj (json_to_user j_lbl)
     | `A [`String "k_nat_elim"; j_mot; j_z; j_s] -> KNatElim (json_to_con j_mot, json_to_con j_z, json_to_con j_s)
     | `A [`String "k_circle_elim"; j_mot; j_b; j_l] -> KCircleElim (json_to_con j_mot, json_to_con j_b, json_to_con j_l)
-    | `String "k-el_out" -> KElOut
     | j -> J.parse_error j "Domain.json_to_frm"
 
   and json_to_unstable_frm : J.value -> D.unstable_frm =
diff --git a/src/core/Syntax.ml b/src/core/Syntax.ml
index bac4d0fe7..0b84f9a2f 100644
--- a/src/core/Syntax.ml
+++ b/src/core/Syntax.ml
@@ -58,9 +58,6 @@ struct
     | CofSplit branches -> Format.fprintf fmt "cof/split[%a]" (Pp.pp_sep_list dump_branch) branches
     | Prf -> Format.fprintf fmt "prf"
 
-    | ElIn tm -> Format.fprintf fmt "el/in[%a]" dump tm
-    | ElOut tm -> Format.fprintf fmt "el/out[%a]" dump tm
-
     | Box _ -> Format.fprintf fmt "<box>"
     | Cap _ -> Format.fprintf fmt "<cap>"
 
@@ -160,7 +157,7 @@ struct
       | NatElim _ | Loop _
       | CircleElim _ -> juxtaposition
 
-      | SubIn _ | SubOut _ | ElIn _ | ElOut _ -> passed
+      | SubIn _ | SubOut _ -> passed
       | CodePi _ -> arrow
       | CodeSg _ -> times
       | CodeSignature _ -> juxtaposition
@@ -330,11 +327,7 @@ struct
       Format.fprintf fmt "sub/in %a" (pp_atomic env) tm
     | SubOut tm when Debug.is_debug_mode () ->
       Format.fprintf fmt "sub/out %a" (pp_atomic env) tm
-    | ElIn tm when Debug.is_debug_mode () ->
-      Format.fprintf fmt "el/in %a" (pp_atomic env) tm
-    | ElOut tm when Debug.is_debug_mode () ->
-      Format.fprintf fmt "el/out %a" (pp_atomic env) tm
-    | SubIn tm | SubOut tm | ElIn tm | ElOut tm ->
+    | SubIn tm | SubOut tm ->
       pp env penv fmt tm
 
     | CodePi (base, fam) when Debug.is_debug_mode () ->
@@ -566,7 +559,7 @@ struct
       Format.fprintf fmt "%a %a"
         Uuseg_string.pp_utf_8 x
         (pp_lambdas envx) tm
-    | (SubIn tm | SubOut tm | ElIn tm | ElOut tm) when not @@ Debug.is_debug_mode () ->
+    | (SubIn tm | SubOut tm) when not @@ Debug.is_debug_mode () ->
       pp_lambdas env fmt tm
     | _ ->
       Format.fprintf fmt "=>@ @[%a@]"
diff --git a/src/core/SyntaxData.ml b/src/core/SyntaxData.ml
index 05485796e..66af9b834 100644
--- a/src/core/SyntaxData.ml
+++ b/src/core/SyntaxData.ml
@@ -42,9 +42,6 @@ struct
     | CofSplit of (t * t) list
     | Prf
 
-    | ElIn of t
-    | ElOut of t
-
     | Box of t * t * t * t * t
     | Cap of t * t * t * t * t
 
diff --git a/src/core/TermBuilder.ml b/src/core/TermBuilder.ml
index ba3f1f824..94ba2353d 100644
--- a/src/core/TermBuilder.ml
+++ b/src/core/TermBuilder.ml
@@ -64,10 +64,6 @@ module MU = Monad.Util (M)
 
 type 'a b = S.t m -> 'a m
 
-let el_in m : _ m =
-  let+ tm = m in
-  S.ElIn tm
-
 let tp_locked_prf mphi : _ m =
   let+ phi = mphi in
   S.TpLockedPrf phi
@@ -83,11 +79,6 @@ let locked_prf_unlock mtp ~cof ~prf ~bdy =
   and+ bdy = bdy in
   S.LockedPrfUnlock {tp; cof; prf; bdy}
 
-
-let el_out m : _ m =
-  let+ tm = m in
-  S.ElOut tm
-
 let lam ?(ident = `Anon) mbdy : _ m =
   scope @@ fun var ->
   let+ bdy = mbdy var in
@@ -424,22 +415,22 @@ struct
   let code_equiv code_a code_b =
     code_sg (code_pi code_a @@ lam @@ fun _ -> code_b) @@ lam @@ fun f ->
     code_pi code_b @@ lam @@ fun y ->
-    code_is_contr @@ code_fiber code_a code_b (el_out f) y
+    code_is_contr @@ code_fiber code_a code_b f y
 
   let equiv_fwd equiv =
-    el_out @@ fst @@ el_out equiv
+    fst equiv
 
   (* CJHM CCHM names *)
   let equiv_fiber_contr equiv y =
-    ap (el_out @@ snd @@ el_out equiv) [y]
+    ap (snd equiv) [y]
 
   (* CJHM CCHM names *)
   let equiv_inv equiv y =
-    fst @@ el_out @@ equiv_fiber_contr equiv y
+    fst @@ equiv_fiber_contr equiv y
 
   (* CJHM CCHM names *)
   let equiv_inv_path equiv y p =
-    ap (el_out @@ snd @@ el_out @@ equiv_fiber_contr equiv y) [p]
+    ap (snd @@ equiv_fiber_contr equiv y) [p]
 end
 
 module Kan =
@@ -448,29 +439,26 @@ struct
   type hcom = r:S.t m -> r':S.t m -> phi:S.t m -> bdy:S.t m -> S.t m
 
   let coe_pi ~base_line ~fam_line ~r ~r' ~bdy : _ m =
-    el_in @@
     lam @@ fun arg ->
     let_ (lam @@ fun i -> coe base_line r' i arg) @@ fun coe_base_line ->
     let fib_line = lam @@ fun i -> ap fam_line [i; ap coe_base_line [i]] in
     coe fib_line r r' @@
-    ap (el_out bdy) [ap coe_base_line [r]]
+    ap bdy [ap coe_base_line [r]]
 
   let hcom_pi ~fam ~r ~r' ~phi ~bdy : _ m =
-    el_in @@
     lam @@ fun arg ->
     let tfib = ap fam [arg] in
     hcom tfib r r' phi @@
     lam @@ fun i ->
     lam @@ fun prf ->
-    ap (el_out (ap bdy [i; prf])) [arg]
+    ap (ap bdy [i; prf]) [arg]
 
   let coe_sg ~base_line ~fam_line ~r ~r' ~bdy : _ m =
-    let fst_line = lam @@ fun i -> coe base_line r i @@ fst @@ el_out bdy in
+    let fst_line = lam @@ fun i -> coe base_line r i @@ fst @@ bdy in
     let fib_line = lam @@ fun i -> ap fam_line [i; ap fst_line [i]] in
-    el_in @@
     pair
       (ap fst_line [r'])
-      (coe fib_line r r' @@ snd @@ el_out bdy)
+      (coe fib_line r r' @@ snd @@ bdy)
 
   let hcom_sg ~base ~fam ~r ~r' ~phi ~bdy : _ m =
     let p0_line =
@@ -478,7 +466,7 @@ struct
       hcom base r i phi @@
       lam @@ fun j ->
       lam @@ fun prf ->
-      fst @@ el_out @@ ap bdy [j; prf]
+      fst @@ ap bdy [j; prf]
     in
     let p0 = ap p0_line [r'] in
     let fib_line =
@@ -489,19 +477,18 @@ struct
       com fib_line r r' phi @@
       lam @@ fun i ->
       lam @@ fun prf ->
-      snd @@ el_out @@ ap bdy [i; prf]
+      snd @@ ap bdy [i; prf]
     in
-    el_in @@
     pair p0 p1
 
   let coe_sign ~field_lines ~r ~r' ~bdy : _ m =
     let mk_line bound_lines (lbl, fam_line) =
       let fib_line = lam @@ fun i -> ap fam_line (i :: List.map (fun (_, line) -> ap line [i]) bound_lines) in
-      let line = lam @@ fun i -> coe fib_line r i @@ proj (el_out bdy) lbl in
+      let line = lam @@ fun i -> coe fib_line r i @@ proj bdy lbl in
       bound_lines @ [(lbl, line)]
     in
     let field_coe_lines = List.fold_left mk_line [] field_lines in
-    el_in @@ struct_ @@ List.map (fun (lbl, fam_line) -> lbl, ap fam_line [r']) field_coe_lines
+    struct_ @@ List.map (fun (lbl, fam_line) -> lbl, ap fam_line [r']) field_coe_lines
 
   let hcom_sign ~fields ~r ~r' ~phi ~bdy : _ m =
     let mk_line bound_lines (lbl, fam) =
@@ -528,10 +515,9 @@ struct
           proj (ap bdy [j; prf]) lbl
         in List.fold_left mk_line [(lbl, p0_line)] fields
     in
-    el_in @@ struct_ @@ List.map (fun (lbl, p_line) -> lbl, ap p_line [r']) lines
+    struct_ @@ List.map (fun (lbl, p_line) -> lbl, ap p_line [r']) lines
 
   let coe_ext ~n ~cof ~fam_line ~bdry_line ~r ~r' ~bdy =
-    el_in @@
     nlam n @@ fun js ->
     sub_in @@
     let_ (ap cof js) @@ fun cof_js ->
@@ -540,10 +526,9 @@ struct
     lam @@ fun _ ->
     cof_split
       [cof_js, ap bdry_line @@ i :: js @ [prf]
-      ; eq i r, sub_out @@ ap (el_out bdy) js]
+      ; eq i r, sub_out @@ ap bdy js]
 
   let hcom_ext ~n ~cof ~fam ~bdry ~r ~r' ~phi ~bdy =
-    el_in @@
     nlam n @@ fun js ->
     sub_in @@
     let_ (ap cof js) @@ fun cof_js ->
@@ -553,7 +538,7 @@ struct
     lam @@ fun _p ->
     cof_split
       [ cof_js, ap bdry @@ js @ [prf]
-      ; join [phi; eq k r], sub_out @@ ap (el_out (ap bdy [k; prf])) js
+      ; join [phi; eq k r], sub_out @@ ap (ap bdy [k; prf]) js
       ]
 
   module V :
@@ -618,19 +603,19 @@ struct
               (coe (lam code_) r i (ap f_tilde [r; prf; bdy]))
           in
           lam @@ fun _ ->
-          coe line r r' @@ el_in @@ lam @@ fun _ -> sub_in @@ ap f_tilde [r; prf; bdy]
+          coe line r r' @@ lam @@ fun _ -> sub_in @@ ap f_tilde [r; prf; bdy]
         end
       @@ fun r_tilde ->
       let_ ~ident:(`Machine "S")
         begin
           lam @@ fun _ ->
           Equiv.equiv_inv_path (ap (pequiv_ r') [prf]) o_tilde @@ (* "q_tilde" *)
-          el_in @@ cof_split
+          cof_split
             [forall (fun i -> eq (s_ i) dim0), pair
                (coe (lam @@ fun j -> ap (pcode_ j) [prf]) r r' bdy)
                (ap r_tilde [prf]);
              eq r r', pair bdy
-               (el_in @@ lam @@ fun _ -> sub_in @@ vproj (s_ r) (pcode_ r) (code_ r) (pequiv_ r) bdy)]
+               (lam @@ fun _ -> sub_in @@ vproj (s_ r) (pcode_ r) (code_ r) (pequiv_ r) bdy)]
         end
       @@ fun s_tilde ->
       let_ ~ident:(`Machine "T")
@@ -641,7 +626,7 @@ struct
           lam @@ fun _ ->
           cof_split
             [eq j dim0, Equiv.equiv_inv (ap (pequiv_ r') [prf]) o_tilde; (* "p_tilde" *)
-             join [forall (fun i -> eq (s_ i) dim0); eq r r'], sub_out @@ ap (el_out @@ ap s_tilde [prf]) [j]]
+             join [forall (fun i -> eq (s_ i) dim0); eq r r'], sub_out @@ ap (ap s_tilde [prf]) [j]]
         end
       @@ fun t_tilde ->
       let_ ~ident:(`Machine "U")
@@ -651,10 +636,10 @@ struct
           lam @@ fun _ ->
           cof_split
             [join [eq k dim1; eq r r'], o_tilde;
-             eq (s_ r') dim0, sub_out @@ ap (el_out @@ snd @@ el_out @@ ap t_tilde [prf]) [k]]
+             eq (s_ r') dim0, sub_out @@ ap (snd @@ ap t_tilde [prf]) [k]]
         end
       @@ fun u_tilde ->
-      vin (s_ r') (pequiv_ r') (lam @@ fun _ -> fst @@ el_out @@ ap t_tilde [prf]) u_tilde
+      vin (s_ r') (pequiv_ r') (lam @@ fun _ -> fst @@ ap t_tilde [prf]) u_tilde
   end
 
   module FHCom :
diff --git a/src/core/TermBuilder.mli b/src/core/TermBuilder.mli
index b2f0e557e..c706ae8ae 100644
--- a/src/core/TermBuilder.mli
+++ b/src/core/TermBuilder.mli
@@ -50,9 +50,6 @@ val tm_abort : t m
 val sub_out : t m -> t m
 val sub_in : t m -> t m
 
-val el_in : t m -> t m
-val el_out : t m -> t m
-
 val univ : tp m
 val nat : tp m
 val code_nat : t m
diff --git a/src/frontend/Tactics.ml b/src/frontend/Tactics.ml
index c93a1e50a..bea40ea20 100644
--- a/src/frontend/Tactics.ml
+++ b/src/frontend/Tactics.ml
@@ -115,14 +115,8 @@ let rec intro_subtypes_and_total : T.Chk.tac -> T.Chk.tac =
     RM.ret tac
 
 let intro_conversions (tac : T.Syn.tac) : T.Chk.tac =
-  (* HACK: Because we are using Weak Tarski Universes, we can't just
-     use the conversion checker to equate 'tp` and 'univ', as
-     'tp' may be 'el code-univ' instead.
-
-     Therefore, we do an explicit check here instead.
-     If we add universe levels, this code should probably be reconsidered. *)
   T.Chk.rule ~name:"intro_conversions" @@ function
-  | D.Univ | D.ElStable `Univ as tp ->
+  | D.Univ as tp ->
     let* tm, tp' = T.Syn.run tac in
     let* vtm = RM.lift_ev @@ Sem.eval tm in
     begin
@@ -130,12 +124,10 @@ let intro_conversions (tac : T.Syn.tac) : T.Chk.tac =
       | D.Pi (D.ElStable (`Signature vsign) as base, ident, clo) ->
         let* tac' = T.abstract ~ident base @@ fun var ->
           let* fam = RM.lift_cmp @@ Sem.inst_tp_clo clo (T.Var.con var) in
-          let* fam = RM.lift_cmp @@ Sem.whnf_tp_ ~style:`UnfoldAll fam in
-          (* Same HACK *)
-          match fam with
-          | D.Univ
-          | D.ElStable `Univ -> RM.ret @@ R.Univ.total vsign vtm
-          | _ -> RM.ret @@ T.Chk.syn tac
+          let* conv = RM.trap @@ RM.lift_conv_ @@ Conversion.equate_tp fam D.Univ in
+          match conv with
+          | Ok () -> RM.ret @@ R.Univ.total vsign vtm
+          | Error _ -> RM.ret @@ T.Chk.syn tac
         in
         T.Chk.run tac' tp
       | _ -> T.Chk.run (T.Chk.syn tac) tp
@@ -166,7 +158,7 @@ struct
     let* tscrut, ind_tp = T.Syn.run scrut in
     let scrut = T.Syn.rule @@ RM.ret (tscrut, ind_tp) (* only makes sense because because I know 'scrut' won't be used under some binder *) in
     match ind_tp, mot with
-    | D.Nat, mot ->
+    | (D.Nat | D.ElStable `Nat) , mot ->
       let* tac_zero : T.Chk.tac =
         match find_case ["zero"] cases with
         | Some ([], tac) -> RM.ret tac
@@ -183,7 +175,7 @@ struct
         | None -> RM.ret @@ R.Hole.unleash_hole @@ Some "suc"
       in
       T.Syn.run @@ R.Nat.elim mot tac_zero tac_suc scrut
-    | D.Circle, mot ->
+    | (D.Circle | D.ElStable `Circle), mot ->
       let* tac_base : T.Chk.tac =
         match find_case ["base"] cases with
         | Some ([], tac) -> RM.ret tac
@@ -221,7 +213,7 @@ struct
       let mot_tac : T.Chk.tac =
         R.Pi.intro @@ fun var -> (* of inductive type *)
         T.Chk.brule @@ fun _goal ->
-        let* fib = RM.lift_cmp @@ Sem.inst_tp_clo fam @@ D.ElIn (T.Var.con var) in
+        let* fib = RM.lift_cmp @@ Sem.inst_tp_clo fam @@ T.Var.con var in
         let* tfib = RM.quote_tp fib in
         match tfib with
         | S.El code ->
@@ -233,7 +225,7 @@ struct
       R.Pi.intro @@ fun x ->
       T.Chk.syn @@
       elim mot_tac cases @@
-      R.El.elim @@ T.Var.syn x
+      T.Var.syn x
     | _ ->
       RM.expected_connective `Pi tp
 end
@@ -289,15 +281,14 @@ struct
       Splice.con p @@ fun p ->
       Splice.con q @@ fun q ->
       Splice.term @@
-      TB.el_in @@
       TB.lam @@ fun i ->
       TB.sub_in @@
       TB.hcom code TB.dim0 TB.dim1 (TB.boundary i) @@
       TB.lam @@ fun j ->
       TB.lam @@ fun _ ->
       TB.cof_split [
-        TB.join [TB.eq j TB.dim0; TB.eq i TB.dim0], TB.sub_out @@ TB.ap (TB.el_out p) [i];
-        TB.eq i TB.dim1, TB.sub_out @@ TB.ap (TB.el_out q) [j]
+        TB.join [TB.eq j TB.dim0; TB.eq i TB.dim0], TB.sub_out @@ TB.ap p [i];
+        TB.eq i TB.dim1, TB.sub_out @@ TB.ap q [j]
       ]
     in
     let+ tpath = RM.quote_con path_tp path in
@@ -321,7 +312,6 @@ struct
       Sem.splice_tm @@
       Splice.con x @@ fun x ->
       Splice.term @@
-      TB.el_in @@
       TB.lam @@ fun _ -> TB.sub_in @@ x
     in
     let+ trefl = RM.quote_con refl_tp refl in