diff --git a/tactics/cbn.ml b/tactics/cbn.ml
index 78da1d0bc60f..0570526b474d 100644
--- a/tactics/cbn.ml
+++ b/tactics/cbn.ml
@@ -12,7 +12,6 @@ open Util
 open Names
 open Constr
 open Context
-open Termops
 open Univ
 open Environ
 open EConstr
@@ -28,7 +27,7 @@ open Context.Rel.Declaration
 (** Machinery to custom the behavior of the reduction *)
 module ReductionBehaviour = Reductionops.ReductionBehaviour
 
-type volatile = { volatile : bool } [@@unboxed]
+type cst_info = { volatile : bool; alias : bool; refold_after_iota : bool }
 
 (** Machinery about stack of unfolded constants *)
 module Cst_stack = struct
@@ -39,10 +38,19 @@ module Cst_stack = struct
 - constant applied to params = term in head applied to args
 - there is at most one arguments with an empty list of args, it must be the first.
 - in args, the int represents the indice of the first arg to consider *)
-  type t = (constr * constr list * (int * constr array) list * volatile)  list
+  type 'a t = (constr * 'a list * (int * 'a array) list * cst_info)  list
 
   let empty = []
-  let all_volatile = CList.for_all (fun (_,_,_,{volatile}) -> volatile)
+  let all_volatile l = CList.for_all (fun (_,_,_,{volatile; _}) -> volatile) l
+  let may_refold_alias_after_iota = function
+    | (_,_,_,{alias=true; refold_after_iota=true; _}) :: _ -> true
+    | [] | (_,_,_,{alias=false; _}) :: _
+    | (_,_,_,{alias=true; refold_after_iota=false; _}) :: _ -> false
+  let mark_alias ?(refold_after_iota=false) = function
+    | (c, params, args, info) :: l ->
+      (c, params, args,
+       { info with alias = true; refold_after_iota = info.refold_after_iota || refold_after_iota }) :: l
+    | [] -> []
 
   let drop_useless = function
     | _ :: ((_,_,[],_)::_ as q) -> q
@@ -61,38 +69,198 @@ module Cst_stack = struct
   let add_args cl =
     List.map (fun (a,b,args,vol) -> (a,b,(0,cl)::args,vol))
 
-  let add_cst ?(volatile=false) cst = function
+  let add_cst ?(volatile=false) ?(refold_after_iota=false) cst = function
     | (_,_,[],_) :: q as l -> l
-    | l -> (cst,[],[],{volatile})::l
+    | l -> (cst,[],[],{volatile; alias=false; refold_after_iota})::l
 
   let best_cst = function
     | (cst,params,[],_)::_ -> Some(cst,params)
     | _ -> None
 
-  let reference sigma t = match best_cst t with
-    | Some (c, params) when isConst sigma c -> Some (fst (destConst sigma c), params)
+  let reference sigma force t = match best_cst t with
+    | Some (c, params) when isConst sigma c -> Some (fst (destConst sigma c), List.map force params)
     | _ -> None
 
   (** [best_replace d cst_l c] makes the best replacement for [d]
       by [cst_l] in [c] *)
-  let best_replace sigma d cst_l c =
+  let best_replace sigma force d cst_l c =
     let reconstruct_head = List.fold_left
-      (fun t (i,args) -> mkApp (t,Array.sub args i (Array.length args - i))) in
+      (fun t (i,args) ->
+         let args = Array.map force (Array.sub args i (Array.length args - i)) in
+         mkApp (t,args)) in
     List.fold_right
       (fun (cst,params,args,_) t -> Termops.replace_term sigma
         (reconstruct_head d args)
-        (applist (cst, List.rev params))
+        (applist (cst, List.rev_map force params))
         t) cst_l c
 
-  let pr env sigma l =
+  let pr env sigma pr_a l =
     let open Pp in
     let p_c c = Termops.Internal.print_constr_env env sigma c in
     prlist_with_sep pr_semicolon
-      (fun (c,params,args,{volatile}) ->
-        hov 1 (str"(" ++ p_c c ++ str ")" ++ spc () ++ pr_sequence p_c params ++ spc () ++ str "(args:" ++
-                 pr_sequence (fun (i,el) -> prvect_with_sep spc p_c (Array.sub el i (Array.length el - i))) args ++
+      (fun (c,params,args,{volatile; alias; refold_after_iota}) ->
+        hov 1 (str"(" ++ p_c c ++ str ")" ++ spc () ++ pr_sequence pr_a params ++ spc () ++ str "(args:" ++
+                 pr_sequence (fun (i,el) -> prvect_with_sep spc pr_a (Array.sub el i (Array.length el - i))) args ++
                str ")" ++
-              (if volatile then str " (volatile)" else mt()))) l
+              (if volatile then str " (volatile)" else mt()) ++
+              (if alias then str " (alias)" else mt()) ++
+              (if refold_after_iota then str " (refold-after-iota)" else mt()))) l
+end
+
+module CbnClos = struct
+  open EConstr
+
+  (* [force] is deliberately cached for non-identity substitutions: several
+     refolding/progress checks compare the same delayed closure repeatedly. *)
+  type t = { term : constr; subst : t Esubst.subs; mutable forced : constr option }
+
+  type view = (t, t, ESorts.t, EInstance.t, ERelevance.t) Constr.kind_of_term
+
+  let id_subst = Esubst.subs_id 0
+  let inject term = { term; subst = id_subst; forced = None }
+  let mk_clos subst term =
+    if Esubst.is_subs_id subst then inject term else { term; subst; forced = None }
+  let mk_clos_vect subst v = Array.map (mk_clos subst) v
+  let lift n c =
+    if Int.equal n 0 then c else { term = c.term; subst = Esubst.subs_shft (n, c.subst); forced = None }
+  let liftn n c =
+    if Int.equal n 0 then c else { term = c.term; subst = Esubst.subs_liftn n c.subst; forced = None }
+  let is_id_subst c = Esubst.is_subs_id c.subst
+  let subst_cons v c = mk_clos (Esubst.subs_cons v c.subst) c.term
+
+  (* Closure-level application used by internal continuations that need to keep
+     constructor/constant spines without forcing all arguments. *)
+  let mk_app f args =
+    match args with
+    | [] -> f
+    | _ :: _ ->
+      let nargs = List.length args in
+      let term = mkApp (mkRel 1, Array.init nargs (fun i -> mkRel (i + 2))) in
+      let subst = List.fold_right Esubst.subs_cons (f :: args) id_subst in
+      mk_clos subst term
+
+  let mk_array u elems def ty =
+    let n = Array.length elems in
+    let term = mkArray (u, Array.init n (fun i -> mkRel (i + 1)), mkRel (n + 1), mkRel (n + 2)) in
+    let subst = List.fold_right Esubst.subs_cons (Array.to_list elems @ [def; ty]) id_subst in
+    mk_clos subst term
+
+  type array_view = {
+    array_length : int;
+    array_get : int -> t;
+    array_default : t;
+  }
+
+  let rec array_view sigma c =
+    match EConstr.kind sigma c.term with
+    | Rel n ->
+      begin match Esubst.expand_rel n c.subst with
+      | Inl (k, v) -> array_view sigma (lift k v)
+      | Inr _ -> None
+      end
+    | Cast (b, _, _) -> array_view sigma (mk_clos c.subst b)
+    | Array (u, elems, def, ty) ->
+      let subst = c.subst in
+      Some {
+        array_length = Array.length elems;
+        array_get = (fun i -> mk_clos subst elems.(i));
+        array_default = mk_clos subst def;
+      }
+    | _ -> None
+
+  let rec force sigma c =
+    if Esubst.is_subs_id c.subst then c.term
+    else match c.forced with
+    | Some t -> t
+    | None ->
+      let t = EConstr.Vars.esubst (fun k v -> force sigma (lift k v)) c.subst c.term in
+      c.forced <- Some t;
+      t
+
+  let force_vect sigma v = Array.map (force sigma) v
+  let force_under sigma n c = force sigma (liftn n c)
+  let force_under_vect sigma n v = Array.map (force_under sigma n) v
+
+  let force_invert sigma = function
+    | NoInvert -> NoInvert
+    | CaseInvert { indices } -> CaseInvert { indices = force_vect sigma indices }
+
+  let force_return sigma ((nas, p), r) =
+    ((nas, force_under sigma (Array.length nas) p), r)
+
+  let force_branch sigma (nas, b) =
+    (nas, force_under sigma (Array.length nas) b)
+
+  let force_branches sigma brs = Array.map (force_branch sigma) brs
+
+  let force_fix sigma ((ri, n), (names, types, bodies)) =
+    let nb = Array.length bodies in
+    ((ri, n), (names, force_vect sigma types, force_under_vect sigma nb bodies))
+
+  let force_cofix sigma (n, (names, types, bodies)) =
+    let nb = Array.length bodies in
+    (n, (names, force_vect sigma types, force_under_vect sigma nb bodies))
+
+  let map_invert subst = function
+    | NoInvert -> NoInvert
+    | CaseInvert { indices } -> CaseInvert { indices = mk_clos_vect subst indices }
+
+  (* If [c] is syntactically a substituted de Bruijn variable, return the
+     substituted value without weak-head reducing that value.  This is used to
+     recognize wrappers such as [fun x => x] without speculatively reducing
+     their arguments. *)
+  let rec subst_value sigma c =
+    match EConstr.kind sigma c.term with
+    | Rel n ->
+      begin match Esubst.expand_rel n c.subst with
+      | Inl (k, v) -> Some (lift k v)
+      | Inr _ -> None
+      end
+    | Cast (b, _, _) -> subst_value sigma (mk_clos c.subst b)
+    | _ -> None
+
+  let equal sigma a b =
+    a == b || (a.term == b.term && a.subst == b.subst) ||
+    (* TODO: add fast path that returns false on non-Rel terms whose head is not of the same shape.
+       Alternatively, fuse the equality check and the substitution *)
+    let a = force sigma a in
+    let b = force sigma b in
+    a == b || EConstr.eq_constr sigma a b
+
+  let equal_under sigma n a b = equal sigma (liftn n a) (liftn n b)
+
+  let rec kind sigma c : view =
+    match EConstr.kind sigma c.term with
+    | Rel n ->
+      begin match Esubst.expand_rel n c.subst with
+      | Inl (k, v) -> kind sigma (lift k v)
+      | Inr (k, _) -> Rel k
+      end
+    | Var id -> Var id
+    | Meta mv -> Meta mv
+    | Evar (ev, args) -> Evar (ev, SList.Skip.map (mk_clos c.subst) args)
+    | Sort s -> Sort s
+    | Cast (b, k, t) -> Cast (mk_clos c.subst b, k, mk_clos c.subst t)
+    | Prod (na, t, b) -> Prod (na, mk_clos c.subst t, mk_clos c.subst b)
+    | Lambda (na, t, b) -> Lambda (na, mk_clos c.subst t, mk_clos c.subst b)
+    | LetIn (na, b, t, c') -> LetIn (na, mk_clos c.subst b, mk_clos c.subst t, mk_clos c.subst c')
+    | App (f, args) -> App (mk_clos c.subst f, mk_clos_vect c.subst args)
+    | Const cst -> Const cst
+    | Ind ind -> Ind ind
+    | Construct cstr -> Construct cstr
+    | Case (ci, u, pms, ((nas, p), r), iv, d, brs) ->
+      let p = ((nas, mk_clos c.subst p), r) in
+      let brs = Array.map (fun (nas, b) -> (nas, mk_clos c.subst b)) brs in
+      Case (ci, u, mk_clos_vect c.subst pms, p, map_invert c.subst iv, mk_clos c.subst d, brs)
+    | Fix ((ri, n), (names, types, bodies)) ->
+      Fix ((ri, n), (names, mk_clos_vect c.subst types, mk_clos_vect c.subst bodies))
+    | CoFix (n, (names, types, bodies)) ->
+      CoFix (n, (names, mk_clos_vect c.subst types, mk_clos_vect c.subst bodies))
+    | Proj (p, r, c') -> Proj (p, r, mk_clos c.subst c')
+    | Int i -> Int i
+    | Float f -> Float f
+    | String s -> String s
+    | Array (u, t, def, ty) -> Array (u, mk_clos_vect c.subst t, mk_clos c.subst def, mk_clos c.subst ty)
 end
 
 
@@ -110,16 +278,17 @@ sig
     case_info * EInstance.t * 'a array * ('a,ERelevance.t) pcase_return * 'a pcase_invert * ('a,ERelevance.t) pcase_branch array
   type 'a member =
   | App of 'a app_node
-  | Case of 'a case_stk * Cst_stack.t
-  | Proj of Projection.t * ERelevance.t * Cst_stack.t
-  | Fix of ('a, 'a, ERelevance.t) pfixpoint * 'a t * Cst_stack.t
-  | Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red * Cst_stack.t
+  | Case of 'a case_stk * 'a Cst_stack.t
+  | Proj of Projection.t * ERelevance.t * 'a Cst_stack.t
+  | Fix of ('a, 'a, ERelevance.t) pfixpoint * 'a t * 'a Cst_stack.t
+  | Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red * 'a Cst_stack.t
   | Cst of { const : cst_member;
              curr : int;
              remains : int list;
              params : 'a t;
              volatile : bool;
-             cst_l : Cst_stack.t;
+             refold_after_iota : bool;
+             cst_l : 'a Cst_stack.t;
            }
 
   and 'a t = 'a member list
@@ -133,12 +302,19 @@ sig
   val strip_app : 'a t -> 'a t * 'a t
   val strip_n_app : int -> 'a t -> ('a t * 'a * 'a t) option
   val will_expose_iota : 'a t -> bool
-  val list_of_app_stack : constr t -> constr list option
+  val list_of_app_stack : 'a t -> 'a list option
+  val app_stack_for_all : ('a -> bool) -> 'a t -> bool
   val args_size : 'a t -> int
   val tail : int -> 'a t -> 'a t
   val nth : 'a t -> int -> 'a
-  val best_state : Evd.evar_map -> constr * constr t -> Cst_stack.t -> constr * constr t
-  val zip : ?refold:bool -> Evd.evar_map -> constr * constr t -> constr
+  val best_state : inject:(constr -> 'a) -> equal:('a -> 'a -> bool) -> 'a * 'a t -> 'a Cst_stack.t -> 'a * 'a t
+  val zip : ?refold:bool -> Evd.evar_map ->
+    force:('a -> constr) ->
+    force_return:(('a,ERelevance.t) pcase_return -> (constr,ERelevance.t) pcase_return) ->
+    force_invert:('a pcase_invert -> constr pcase_invert) ->
+    force_branch:(('a,ERelevance.t) pcase_branch -> (constr,ERelevance.t) pcase_branch) ->
+    force_fix:(('a, 'a, ERelevance.t) pfixpoint -> (constr, constr, ERelevance.t) pfixpoint) ->
+    inject:(constr -> 'a) -> equal:('a -> 'a -> bool) -> 'a * 'a t -> constr
   val check_native_args : CPrimitives.t -> 'a t -> bool
   val get_next_primitive_args : CPrimitives.args_red -> 'a t -> CPrimitives.args_red * ('a t * 'a * 'a t) option
 end =
@@ -148,10 +324,9 @@ struct
   (* first releavnt position, arguments, last relevant position *)
 
   (*
-     Invariant that this module must ensure :
-     (behare of direct access to app_node by the rest of Reductionops)
+     Invariant that this module must ensure:
      - in app_node (i,_,j) i <= j
-     - There is no array realocation (outside of debug printing)
+     - There is no array reallocation (outside of debug printing)
    *)
 
   let pr_app_node pr (i,a,j) =
@@ -168,16 +343,17 @@ struct
     case_info * EInstance.t * 'a array * ('a,ERelevance.t) pcase_return * 'a pcase_invert * ('a,ERelevance.t) pcase_branch array
   type 'a member =
   | App of 'a app_node
-  | Case of 'a case_stk * Cst_stack.t
-  | Proj of Projection.t * ERelevance.t * Cst_stack.t
-  | Fix of ('a, 'a, ERelevance.t) pfixpoint * 'a t * Cst_stack.t
-  | Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red * Cst_stack.t
+  | Case of 'a case_stk * 'a Cst_stack.t
+  | Proj of Projection.t * ERelevance.t * 'a Cst_stack.t
+  | Fix of ('a, 'a, ERelevance.t) pfixpoint * 'a t * 'a Cst_stack.t
+  | Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red * 'a Cst_stack.t
   | Cst of { const : cst_member;
              curr : int;
              remains : int list;
              params : 'a t;
              volatile : bool;
-             cst_l : Cst_stack.t;
+             refold_after_iota : bool;
+             cst_l : 'a Cst_stack.t;
            }
 
   and 'a t = 'a member list
@@ -200,11 +376,12 @@ struct
     | Primitive (p,c,args,kargs,cst_l) ->
       str "ZPrimitive(" ++ str (CPrimitives.to_string p)
       ++ pr_comma () ++ pr pr_c args ++ str ")"
-    | Cst {const=mem;curr;remains;params;cst_l} ->
+    | Cst {const=mem;curr;remains;params;cst_l;refold_after_iota} ->
       str "ZCst(" ++ pr_cst_member pr_c mem ++ pr_comma () ++ int curr
       ++ pr_comma () ++
         prlist_with_sep pr_semicolon int remains ++
-        pr_comma () ++ pr pr_c params ++ str ")"
+        pr_comma () ++ pr pr_c params ++
+        (if refold_after_iota then str ", refold-after-iota" else mt()) ++ str ")"
   and pr pr_c l =
     let open Pp in
     prlist_with_sep pr_semicolon (fun x -> hov 1 (pr_member pr_c x)) l
@@ -313,6 +490,15 @@ struct
     let init = match s' with [] -> true | _ -> false in
     Option.init init out
 
+  let app_stack_for_all p s =
+    let rec aux = function
+      | App (i,a,j) :: s ->
+        let rec loop k = k > j || (p a.(k) && loop (succ k)) in
+        loop i && aux s
+      | [] -> true
+      | _ :: _ -> false
+    in aux s
+
   let tail n0 s0 =
     let rec aux n s =
       if Int.equal n 0 then s else
@@ -333,50 +519,87 @@ struct
     | None -> raise Not_found
 
   (** This function breaks the abstraction of Cst_stack ! *)
-  let best_state sigma (_,sk as s) l =
+  let best_state_opt ~inject ~equal sk l =
     let rec aux sk def = function
-      |(_,_,_,{volatile=true}) -> def
-      |(cst, params, [], _) -> (cst, append_app_list (List.rev params) sk)
+      |(_,_,_,{volatile=true; _}) -> def
+      |(cst, params, [], _) -> Some (inject cst, append_app_list (List.rev params) sk)
       |(cst, params, (i,t)::q, vol) -> match decomp sk with
-        | Some (el,sk') when EConstr.eq_constr sigma el t.(i) ->
+        | Some (el,sk') when equal el t.(i) ->
           if i = pred (Array.length t)
           then aux sk' def (cst, params, q, vol)
           else aux sk' def (cst, params, (succ i,t)::q, vol)
         | _ -> def
-    in List.fold_left (aux sk) s l
+    in List.fold_left (aux sk) None l
+
+  let best_state ~inject ~equal (_,sk as s) l =
+    match best_state_opt ~inject ~equal sk l with
+    | Some s -> s
+    | None -> s
 
-  let constr_of_cst_member f sk =
+  let constr_of_cst_member force inject f sk =
     match f with
-    | Cst_const (c, u) -> mkConstU (c, EInstance.make u), sk
+    | Cst_const (c, u) -> inject (mkConstU (c, EInstance.make u)), sk
     | Cst_proj (p,r) ->
       match decomp sk with
-      | Some (hd, sk) -> mkProj (p, r, hd), sk
+      | Some (hd, sk) -> inject (mkProj (p, r, force hd)), sk
       | None -> assert false
 
-  let zip ?(refold=false) sigma s =
+  let zip ?(refold=false) sigma ~force ~force_return ~force_invert ~force_branch ~force_fix ~inject ~equal s =
+  (* [best_state_opt] only inspects the residual stack.  Try it before
+     materializing eliminated terms: on success the reconstructed case/fix/proj
+     would be discarded immediately. *)
+  let best_refold = best_state_opt ~inject ~equal in
   let rec zip = function
-    | f, [] -> f
+    | f, [] -> force f
     | f, (App (i,a,j) :: s) ->
        let a' = if Int.equal i 0 && Int.equal j (Array.length a - 1)
                 then a
                 else Array.sub a i (j - i + 1) in
-       zip (mkApp (f, a'), s)
+       zip (inject (mkApp (force f, Array.map force a')), s)
     | f, (Case ((ci,u,pms,rt,iv,br),cst_l)::s) when refold ->
-      zip (best_state sigma (mkCase (ci,u,pms,rt,iv,f,br), s) cst_l)
-    | f, (Case ((ci,u,pms,rt,iv,br),_)::s) -> zip (mkCase (ci,u,pms,rt,iv,f,br), s)
+      begin match best_refold s cst_l with
+      | Some state -> zip state
+      | None ->
+        let case = mkCase (ci,u,Array.map force pms,force_return rt,force_invert iv,force f,Array.map force_branch br) in
+        zip (inject case, s)
+      end
+    | f, (Case ((ci,u,pms,rt,iv,br),_)::s) ->
+      zip (inject (mkCase (ci,u,Array.map force pms,force_return rt,force_invert iv,force f,Array.map force_branch br)), s)
     | f, (Fix (fix,st,cst_l)::s) when refold ->
-      zip (best_state sigma (mkFix fix, st @ (append_app [|f|] s)) cst_l)
+      let sk = st @ append_app [|f|] s in
+      begin match best_refold sk cst_l with
+      | Some state -> zip state
+      | None -> zip (inject (mkFix (force_fix fix)), sk)
+      end
   | f, (Fix (fix,st,_)::s) -> zip
-    (mkFix fix, st @ (append_app [|f|] s))
+    (inject (mkFix (force_fix fix)), st @ (append_app [|f|] s))
   | f, (Cst {const;params;cst_l}::s) when refold ->
-    zip (best_state sigma (constr_of_cst_member const (params @ (append_app [|f|] s))) cst_l)
+    let sk = params @ append_app [|f|] s in
+    begin match const with
+    | Cst_const (c, u) ->
+      begin match best_refold sk cst_l with
+      | Some state -> zip state
+      | None -> zip (inject (mkConstU (c, EInstance.make u)), sk)
+      end
+    | Cst_proj (p, r) ->
+      match decomp sk with
+      | Some (hd, sk) ->
+        begin match best_refold sk cst_l with
+        | Some state -> zip state
+        | None -> zip (inject (mkProj (p, r, force hd)), sk)
+        end
+      | None -> assert false
+    end
   | f, (Cst {const;params}::s) ->
-    zip (constr_of_cst_member const (params @ (append_app [|f|] s)))
+    zip (constr_of_cst_member force inject const (params @ (append_app [|f|] s)))
   | f, (Proj (p,r,cst_l)::s) when refold ->
-    zip (best_state sigma (mkProj (p,r,f),s) cst_l)
-  | f, (Proj (p,r,_)::s) -> zip (mkProj (p,r,f),s)
+    begin match best_refold s cst_l with
+    | Some state -> zip state
+    | None -> zip (inject (mkProj (p,r,force f)),s)
+    end
+  | f, (Proj (p,r,_)::s) -> zip (inject (mkProj (p,r,force f)),s)
   | f, (Primitive (p,c,args,kargs,cst_l)::s) ->
-      zip (mkConstU c, args @ append_app [|f|] s)
+      zip (inject (mkConstU c), args @ append_app [|f|] s)
   in
   zip s
 
@@ -409,15 +632,103 @@ end
 
 (* Beta Reduction tools *)
 
-let apply_subst env sigma cst_l t stack =
-  let rec aux env cst_l t stack =
-    match (Stack.decomp stack, EConstr.kind sigma t) with
+let stack_zip ?refold sigma =
+  Stack.zip ?refold sigma
+    ~force:(CbnClos.force sigma)
+    ~force_return:(CbnClos.force_return sigma)
+    ~force_invert:(CbnClos.force_invert sigma)
+    ~force_branch:(CbnClos.force_branch sigma)
+    ~force_fix:(CbnClos.force_fix sigma)
+    ~inject:CbnClos.inject
+    ~equal:(CbnClos.equal sigma)
+
+let clos_of_app_stack sigma x args =
+  if CbnClos.is_id_subst x && Stack.app_stack_for_all CbnClos.is_id_subst args then
+    CbnClos.inject (stack_zip sigma (x,args))
+  else match Stack.list_of_app_stack args with
+  | Some args -> CbnClos.mk_app x args
+  | None -> assert false
+
+let reduce_array_primitive sigma u p args =
+  let get i = Array.get args i in
+  let get_int i = match CbnClos.kind sigma (get i) with
+    | Int i -> Some i
+    | _ -> None
+  in
+  let get_array i = CbnClos.array_view sigma (get i) in
+  let bounded_index len i =
+    if Uint63.le Uint63.zero i && Uint63.lt i (Uint63.of_int len)
+    then Some (snd (Uint63.to_int2 i))
+    else None
+  in
+  let elems_of_array a = Array.init a.CbnClos.array_length a.CbnClos.array_get in
+  let mk_array elems def ty = CbnClos.mk_array u elems def ty in
+  try match p with
+  | CPrimitives.Arraymake ->
+    begin match get_int 1 with
+    | Some len ->
+      let a = Parray.make len (get 2) in
+      let elems, def = Parray.to_array a in
+      Some (mk_array elems def (get 0))
+    | None -> None
+    end
+  | CPrimitives.Arrayget ->
+    begin match get_array 1, get_int 2 with
+    | Some a, Some i ->
+      let elt = match bounded_index a.CbnClos.array_length i with
+        | Some i -> a.CbnClos.array_get i
+        | None -> a.CbnClos.array_default
+      in
+      Some elt
+    | _, _ -> None
+    end
+  | CPrimitives.Arraydefault ->
+    begin match get_array 1 with
+    | Some a -> Some a.CbnClos.array_default
+    | None -> None
+    end
+  | CPrimitives.Arrayset ->
+    begin match get_array 1, get_int 2 with
+    | Some a, Some i ->
+      let elems = match bounded_index a.CbnClos.array_length i with
+        | Some i -> Array.init a.CbnClos.array_length (fun j -> if Int.equal i j then get 3 else a.CbnClos.array_get j)
+        | None -> elems_of_array a
+      in
+      Some (mk_array elems a.CbnClos.array_default (get 0))
+    | _, _ -> None
+    end
+  | CPrimitives.Arraycopy ->
+    begin match get_array 1 with
+    | Some a -> Some (mk_array (elems_of_array a) a.CbnClos.array_default (get 0))
+    | None -> None
+    end
+  | CPrimitives.Arraylength ->
+    begin match get_array 1 with
+    | Some a -> Some (CbnClos.inject (mkInt (Uint63.of_int a.CbnClos.array_length)))
+    | None -> None
+    end
+  | _ -> None
+  with Invalid_argument _ -> None
+
+let apply_subst sigma cst_l t stack =
+  let rec aux cst_l t stack =
+    match (Stack.decomp stack, CbnClos.kind sigma t) with
     | Some (h,stacktl), Lambda (_,_,c) ->
        let cst_l' = Cst_stack.add_param h cst_l in
-       aux (h::env) cst_l' c stacktl
-    | _ -> (cst_l, (substl env t, stack))
+       aux cst_l' (CbnClos.subst_cons h c) stacktl
+    | _ ->
+      let cst_l = match CbnClos.subst_value sigma t with
+        | Some tm ->
+          let refold_after_iota = match stack, CbnClos.kind sigma tm with
+            | _ :: _, (Const _ | Var _ | Rel _) -> true
+            | [], _ | _ :: _, _ -> false
+          in
+          Cst_stack.mark_alias ~refold_after_iota cst_l
+        | None -> cst_l
+      in
+      (cst_l, (t, stack))
   in
-  aux env cst_l t stack
+  aux cst_l t stack
 
 (* Iota reduction tools *)
 
@@ -471,53 +782,91 @@ let magically_constant_of_fixbody env sigma (reference, params) bd = function
           | None -> bd
         end
 
-let contract_cofix env sigma ?reference (bodynum,(names,types,bodies as typedbodies)) =
+let raw_rec_declaration (names, types, bodies) =
+  (names, Array.map (fun c -> c.CbnClos.term) types, Array.map (fun c -> c.CbnClos.term) bodies)
+
+let contract_cofix env sigma ?reference ?current_refold (bodynum,(names,types,bodies as typedbodies)) =
   let nbodies = Array.length bodies in
+  let raw_typedbodies = raw_rec_declaration typedbodies in
+  let base_subst = bodies.(bodynum).CbnClos.subst in
+  let current_refold = Option.map
+      (fun (cst, params) -> CbnClos.mk_app (CbnClos.inject cst) (List.rev params))
+      current_refold in
   let make_Fi j =
     let ind = nbodies-j-1 in
-    if Int.equal bodynum ind then mkCoFix (ind,typedbodies)
-    else
-      let bd = mkCoFix (ind,typedbodies) in
-      match reference with
+    let bd = CbnClos.mk_clos base_subst (mkCoFix (ind,raw_typedbodies)) in
+    if Int.equal bodynum ind then Option.default bd current_refold
+    else match reference with
       | None -> bd
-      | Some r -> magically_constant_of_fixbody env sigma r bd names.(ind).binder_name in
+      | Some r ->
+        CbnClos.inject (magically_constant_of_fixbody env sigma r (CbnClos.force sigma bd) names.(ind).binder_name) in
   let closure = List.init nbodies make_Fi in
-  substl closure bodies.(bodynum)
+  let subst = List.fold_right Esubst.subs_cons closure bodies.(bodynum).CbnClos.subst in
+  CbnClos.mk_clos subst bodies.(bodynum).CbnClos.term
 
 (** Similar to the "fix" case below *)
-let reduce_and_refold_cofix recfun env sigma cst_l cofix sk =
+let singleton_best_cst = function
+  | [_] as cst_l -> Cst_stack.best_cst cst_l
+  | [] | _ :: _ :: _ -> None
+
+let reduce_and_refold_cofix recfun env sigma cst_l ((_,(_,_,bodies)) as cofix) sk =
+  let current_refold = singleton_best_cst cst_l in
+  let reference =
+    if Array.length bodies > 1 then Cst_stack.reference sigma (CbnClos.force sigma) cst_l
+    else None
+  in
   let raw_answer =
-    contract_cofix env sigma ?reference:(Cst_stack.reference sigma cst_l) cofix in
-  let (x, (t, sk')) = apply_subst [] sigma Cst_stack.empty raw_answer sk in
-  let t' = Cst_stack.best_replace sigma (mkCoFix cofix) cst_l t in
-  recfun x (t', sk')
+    contract_cofix env sigma ?reference ?current_refold cofix in
+  let (x, (t, sk')) = apply_subst sigma Cst_stack.empty raw_answer sk in
+  let t = match cst_l, current_refold with
+    | [], _ | _, Some _ -> t
+    | _ :: _, None ->
+      let d = mkCoFix (CbnClos.force_cofix sigma cofix) in
+      CbnClos.inject (Cst_stack.best_replace sigma (CbnClos.force sigma) d cst_l (CbnClos.force sigma t))
+  in
+  recfun x (t, sk')
 
 (* contracts fix==FIX[nl;i](A1...Ak;[F1...Fk]{B1....Bk}) to produce
    Bi[Fj --> FIX[nl;j](A1...Ak;[F1...Fk]{B1...Bk})] *)
 
-let contract_fix env sigma ?reference ((recindices,bodynum),(names,types,bodies as typedbodies)) =
+let contract_fix env sigma ?reference ?current_refold ((recindices,bodynum),(names,types,bodies as typedbodies)) =
     let nbodies = Array.length recindices in
+    let raw_typedbodies = raw_rec_declaration typedbodies in
+    let base_subst = bodies.(bodynum).CbnClos.subst in
+    let current_refold = Option.map
+        (fun (cst, params) -> CbnClos.mk_app (CbnClos.inject cst) (List.rev params))
+        current_refold in
     let make_Fi j =
       let ind = nbodies-j-1 in
-      if Int.equal bodynum ind then mkFix ((recindices,ind),typedbodies)
-      else
-        let bd = mkFix ((recindices,ind),typedbodies) in
-        match reference with
+      let bd = CbnClos.mk_clos base_subst (mkFix ((recindices,ind),raw_typedbodies)) in
+      if Int.equal bodynum ind then Option.default bd current_refold
+      else match reference with
         | None -> bd
-        | Some r -> magically_constant_of_fixbody env sigma r bd names.(ind).binder_name in
+        | Some r -> CbnClos.inject (magically_constant_of_fixbody env sigma r (CbnClos.force sigma bd) names.(ind).binder_name) in
     let closure = List.init nbodies make_Fi in
-    substl closure bodies.(bodynum)
+    let subst = List.fold_right Esubst.subs_cons closure bodies.(bodynum).CbnClos.subst in
+    CbnClos.mk_clos subst bodies.(bodynum).CbnClos.term
 
 (** First we substitute the Rel bodynum by the fixpoint and then we try to
     replace the fixpoint by the best constant from [cst_l]
     Other rels are directly substituted by constants "magically found from the
     context" in contract_fix *)
-let reduce_and_refold_fix recfun env sigma cst_l fix sk =
+let reduce_and_refold_fix recfun env sigma cst_l (((_,_),(_,_,bodies)) as fix) sk =
+  let current_refold = singleton_best_cst cst_l in
+  let reference =
+    if Array.length bodies > 1 then Cst_stack.reference sigma (CbnClos.force sigma) cst_l
+    else None
+  in
   let raw_answer =
-    contract_fix env sigma ?reference:(Cst_stack.reference sigma cst_l) fix in
-  let (x, (t, sk')) = apply_subst [] sigma Cst_stack.empty raw_answer sk in
-  let t' = Cst_stack.best_replace sigma (mkFix fix) cst_l t in
-  recfun x (t', sk')
+    contract_fix env sigma ?reference ?current_refold fix in
+  let (x, (t, sk')) = apply_subst sigma Cst_stack.empty raw_answer sk in
+  let t = match cst_l, current_refold with
+    | [], _ | _, Some _ -> t
+    | _ :: _, None ->
+      let d = mkFix (CbnClos.force_fix sigma fix) in
+      CbnClos.inject (Cst_stack.best_replace sigma (CbnClos.force sigma) d cst_l (CbnClos.force sigma t))
+  in
+  recfun x (t, sk')
 
 module CredNative = Reductionops.CredNative
 
@@ -537,28 +886,46 @@ module CredNative = Reductionops.CredNative
 let debug_RAKAM = Reductionops.debug_RAKAM
 
 let equal_stacks env sigma (x, l) (y, l') =
-  let f_equal x y = eq_constr sigma x y in
-  let eq_fix a b = f_equal (mkFix a) (mkFix b) in
+  let f_equal x y = CbnClos.equal sigma x y in
+  let eq_fix a b =
+    eq_constr sigma (mkFix (CbnClos.force_fix sigma a)) (mkFix (CbnClos.force_fix sigma b)) in
   let eq_case (ci1, u1, pms1, (p1,_), _, br1) (ci2, u2, pms2, (p2,_), _, br2) =
+    let eq_under_ctx (nas1, c1) (nas2, c2) =
+      Int.equal (Array.length nas1) (Array.length nas2) &&
+      CbnClos.equal_under sigma (Array.length nas1) c1 c2
+    in
     Array.equal f_equal pms1 pms2 &&
-    f_equal (snd p1) (snd p2) &&
-    Array.equal (fun (_, c1) (_, c2) -> f_equal c1 c2) br1 br2
+    eq_under_ctx p1 p2 &&
+    Array.equal eq_under_ctx br1 br2
   in
   Stack.equal env f_equal eq_fix eq_case l l' && f_equal x y
 
+let cbn_subst_of_rel_context_instance_list sign args subst =
+  let open Context.Rel.Declaration in
+  let rec aux subst sign l = match sign, l with
+    | LocalAssum _ :: sign', a::args' -> aux (Esubst.subs_cons a subst) sign' args'
+    | LocalDef (_,c,_)::sign', args' ->
+      let c = CbnClos.mk_clos subst c in
+      aux (Esubst.subs_cons c subst) sign' args'
+    | [], [] -> subst
+    | _ -> CErrors.anomaly (Pp.str "Instance and signature do not match.")
+  in aux subst (List.rev sign) args
+
 let apply_branch env sigma (ind, i) args (ci, u, pms, iv, r, lf) =
   let args = Stack.tail ci.ci_npar args in
   let args = Option.get (Stack.list_of_app_stack args) in
   let br = lf.(i - 1) in
+  let body = snd br in
   let subst =
     if Int.equal ci.ci_cstr_nargs.(i - 1) ci.ci_cstr_ndecls.(i - 1) then
       (* No let-bindings *)
-      List.rev args
+      List.fold_left (fun subst arg -> Esubst.subs_cons arg subst) body.CbnClos.subst args
     else
-      let ctx = expand_branch env sigma u pms (ind, i) br in
-      subst_of_rel_context_instance_list ctx args
+      let pms = Array.map (CbnClos.force sigma) pms in
+      let ctx = expand_branch env sigma u pms (ind, i) (fst br, mkProp) in
+      cbn_subst_of_rel_context_instance_list ctx args body.CbnClos.subst
   in
-  Vars.substl subst (snd br)
+  CbnClos.mk_clos subst body.CbnClos.term
 
 
 exception PatternFailure
@@ -575,9 +942,11 @@ let match_sort ps s psubst =
 
 let rec match_arg_pattern whrec env sigma ctx psubst p t =
   let open Declarations in
-  let t' = EConstr.it_mkLambda_or_LetIn t ctx in
   match p with
-  | EHole i -> Partial_subst.add_term i t' psubst
+  | EHole i ->
+      let t = CbnClos.force sigma t in
+      let t' = EConstr.it_mkLambda_or_LetIn t ctx in
+      Partial_subst.add_term i t' psubst
   | EHoleIgnored -> psubst
   | ERigid (ph, es) ->
       let (t, stk), _ = whrec Cst_stack.empty (t, Stack.empty) in
@@ -588,7 +957,7 @@ let rec match_arg_pattern whrec env sigma ctx psubst p t =
       | _ :: _ -> raise PatternFailure
 
 and match_rigid_arg_pattern whrec env sigma ctx psubst p t =
-  match [@ocaml.warning "-4"] p, EConstr.kind sigma t with
+  match [@ocaml.warning "-4"] p, CbnClos.kind sigma t with
   | PHInd (ind, pu), Ind (ind', u) ->
     if QInd.equal env ind ind' then match_einstance sigma pu u psubst else raise PatternFailure
   | PHConstr (constr, pu), Construct (constr', u) ->
@@ -604,6 +973,7 @@ and match_rigid_arg_pattern whrec env sigma ctx psubst p t =
   | PHString s, String s' ->
     if Pstring.equal s s' then psubst else raise PatternFailure
   | PHLambda (ptys, pbod), _ ->
+    let t = CbnClos.force sigma t in
     let ntys, _ = EConstr.decompose_lambda sigma t in
     let na = List.length ntys and np = Array.length ptys in
     if np > na then raise PatternFailure;
@@ -612,10 +982,12 @@ and match_rigid_arg_pattern whrec env sigma ctx psubst p t =
     let tys = Array.of_list @@ List.rev_map snd ntys in
     let na = Array.length tys in
     let contexts_upto = Array.init na (fun i -> List.skipn (na - i) ctx' @ ctx) in
+    let tys = Array.map CbnClos.inject tys in
     let psubst = Array.fold_left3 (fun psubst ctx -> match_arg_pattern whrec env sigma ctx psubst) psubst contexts_upto ptys tys in
-    let psubst = match_arg_pattern whrec env sigma (ctx' @ ctx) psubst pbod body in
+    let psubst = match_arg_pattern whrec env sigma (ctx' @ ctx) psubst pbod (CbnClos.inject body) in
     psubst
   | PHProd (ptys, pbod), _ ->
+    let t = CbnClos.force sigma t in
     let ntys, _ = EConstr.decompose_prod sigma t in
     let na = List.length ntys and np = Array.length ptys in
     if np > na then raise PatternFailure;
@@ -624,8 +996,9 @@ and match_rigid_arg_pattern whrec env sigma ctx psubst p t =
     let tys = Array.of_list @@ List.rev_map snd ntys in
     let na = Array.length tys in
     let contexts_upto = Array.init na (fun i -> List.skipn (na - i) ctx' @ ctx) in
+    let tys = Array.map CbnClos.inject tys in
     let psubst = Array.fold_left3 (fun psubst ctx -> match_arg_pattern whrec env sigma ctx psubst) psubst contexts_upto ptys tys in
-    let psubst = match_arg_pattern whrec env sigma (ctx' @ ctx) psubst pbod body in
+    let psubst = match_arg_pattern whrec env sigma (ctx' @ ctx) psubst pbod (CbnClos.inject body) in
     psubst
   | (PHInd _ | PHConstr _ | PHRel _ | PHInt _ | PHFloat _ | PHString _ | PHSort _ | PHSymbol _), _ -> raise PatternFailure
 
@@ -648,9 +1021,12 @@ and apply_rule whrec env sigma ctx psubst es stk =
       if not @@ QInd.equal env pind ci.ci_ind then raise PatternFailure;
       let dummy = mkProp in
       let psubst = match_einstance sigma pu u psubst in
+      let pms = Array.map (CbnClos.force sigma) pms in
+      let p = CbnClos.force_return sigma p in
+      let brs = CbnClos.force_branches sigma brs in
       let (_, _, _, ((ntys_ret, ret), _), _, _, brs) = EConstr.annotate_case env sigma (ci, u, pms, p, NoInvert, dummy, brs) in
-      let psubst = match_arg_pattern whrec env sigma (ntys_ret @ ctx) psubst pret ret in
-      let psubst = Array.fold_left2 (fun psubst pat (ctx', br) -> match_arg_pattern whrec env sigma (ctx' @ ctx) psubst pat br) psubst pbrs brs in
+      let psubst = match_arg_pattern whrec env sigma (ntys_ret @ ctx) psubst pret (CbnClos.inject ret) in
+      let psubst = Array.fold_left2 (fun psubst pat (ctx', br) -> match_arg_pattern whrec env sigma (ctx' @ ctx) psubst pat (CbnClos.inject br)) psubst pbrs brs in
       apply_rule whrec env sigma ctx psubst e s
   | Declarations.PEProj proj :: e, Stack.Proj (proj', r, cst_l') :: s ->
       if not @@ QProjection.Repr.equal env proj (Projection.repr proj') then raise PatternFailure;
@@ -671,7 +1047,7 @@ let rec apply_rules whrec env sigma u r stk =
       let usubst = UVars.Instance.of_array (qsubst, usubst) in
       let rhsu = subst_instance_constr (EConstr.EInstance.make usubst) (EConstr.of_constr rhs) in
       let rhs' = substl (Array.to_list subst) rhsu in
-      (rhs', stk)
+      (CbnClos.inject rhs', stk)
     with PatternFailure -> apply_rules whrec env sigma u rs stk
 
 
@@ -683,32 +1059,73 @@ let whd_state_gen ?csts flags env sigma =
   let rec whrec cst_l (x, stack) =
     let () = debug_RAKAM (fun () ->
         let open Pp in
-        let pr c = Termops.Internal.print_constr_env env sigma c in
+        let pr c = Termops.Internal.print_constr_env env sigma (CbnClos.force sigma c) in
                (h (str "<<" ++ pr x ++
-                   str "|" ++ cut () ++ Cst_stack.pr env sigma cst_l ++
+                   str "|" ++ cut () ++ Cst_stack.pr env sigma pr cst_l ++
                    str "|" ++ cut () ++ Stack.pr pr stack ++
                    str ">>")))
     in
-    let c0 = EConstr.kind sigma x in
+    let reduce_primitive_value () =
+      match Stack.strip_app stack with
+      | (_, Stack.Primitive(p,(_,u as kn),rargs,kargs,cst_l')::s) ->
+        let more_to_reduce = List.exists (fun k -> CPrimitives.Kwhnf = k) kargs in
+        if more_to_reduce then
+          let (kargs,o) = Stack.get_next_primitive_args kargs s in
+          (* Should not fail because Primitive is put on the stack only if fully applied *)
+          let (before,a,after) = Option.get o in
+          Some (whrec Cst_stack.empty (a,Stack.Primitive(p,kn,rargs @ Stack.append_app [|x|] before,kargs,cst_l')::after))
+        else
+          let n = List.length kargs in
+          let (args,s) = Stack.strip_app s in
+          let (args,extra_args) =
+            try List.chop n args
+            with List.IndexOutOfRange -> (args,[]) (* FIXME probably useless *)
+          in
+          let s = extra_args @ s in
+          let args = Option.get (Stack.list_of_app_stack (rargs @ Stack.append_app [|x|] args)) in
+          let args = Array.of_list args in
+          Some
+            (match reduce_array_primitive sigma u p args with
+             | Some t -> whrec cst_l' (t,s)
+             | None ->
+               let args = Array.map (CbnClos.force sigma) args in
+               match CredNative.red_prim env sigma p u args with
+               | Some t -> whrec cst_l' (CbnClos.inject t,s)
+               | None -> ((CbnClos.inject (mkApp (mkConstU kn, args)), s), cst_l))
+      | _ -> None
+    in
     let fold () =
       let () = debug_RAKAM (fun () ->
           Pp.(str "<><><><><>")) in
-      ((EConstr.of_kind c0, stack),cst_l)
+      ((x, stack),cst_l)
     in
+    (* Resuming a primitive on an array value does not need the full
+       [CbnClos.kind] view of the array; building that view allocates a closure
+       for every element even when [array_get]/[array_length] will discard most
+       of them. *)
+    let early_array_primitive = match Stack.strip_app stack with
+      | _, Stack.Primitive _ :: _ when Option.has_some (CbnClos.array_view sigma x) ->
+        reduce_primitive_value ()
+      | _ -> None
+    in
+    match early_array_primitive with
+    | Some res -> res
+    | None ->
+    let c0 = CbnClos.kind sigma x in
     match c0 with
     | Rel n when RedFlags.red_set flags RedFlags.fDELTA ->
       (match lookup_rel n env with
-      | LocalDef (_,body,_) -> whrec Cst_stack.empty (lift n body, stack)
+      | LocalDef (_,body,_) -> whrec Cst_stack.empty (CbnClos.lift n (CbnClos.inject body), stack)
       | _ -> fold ())
     | Var id when RedFlags.red_set flags (RedFlags.fVAR id) ->
       (match lookup_named id env with
       | LocalDef (_,body,_) ->
-        whrec (Cst_stack.add_cst (mkVar id) cst_l) (body, stack)
+        whrec (Cst_stack.add_cst (mkVar id) cst_l) (CbnClos.inject body, stack)
       | _ -> fold ())
     | Evar _ | Meta _ -> fold ()
     | Const (c,u as const) ->
       Reductionops.reduction_effect_hook env sigma c
-         (lazy (EConstr.to_constr sigma (Stack.zip sigma (x,fst (Stack.strip_app stack)))));
+         (lazy (EConstr.to_constr sigma (stack_zip sigma (x,fst (Stack.strip_app stack)))));
       if RedFlags.red_set flags (RedFlags.fCONST c) then
        let u' = EInstance.kind sigma u in
        match constant_value_in env (c, u') with
@@ -717,7 +1134,7 @@ let whd_state_gen ?csts flags env sigma =
           let body = EConstr.of_constr body in
           (* Looks for ReductionBehaviour *)
             match ReductionBehaviour.get c with
-            | None -> whrec (Cst_stack.add_cst (mkConstU const) cst_l) (body, stack)
+            | None -> whrec (Cst_stack.add_cst (mkConstU const) cst_l) (CbnClos.inject body, stack)
             | Some behavior ->
               begin match behavior with
               | NeverUnfold -> fold ()
@@ -728,42 +1145,109 @@ let whd_state_gen ?csts flags env sigma =
               | UnfoldWhenNoMatch { recargs; nargs } -> (* maybe unfolds *)
                   let app_sk,sk = Stack.strip_app stack in
                   let volatile = Option.has_some nargs in
-                  let (tm',sk'),cst_l' =
-                    match recargs with
-                    | [] ->
-                      whrec (Cst_stack.add_cst ~volatile (mkConstU const) cst_l) (body, app_sk)
-                    | curr :: remains -> match Stack.strip_n_app curr app_sk with
-                      | None -> (x,app_sk), cst_l
-                      | Some (bef,arg,app_sk') ->
-                        let cst_l = Stack.Cst
-                            { const = Stack.Cst_const (fst const, u');
-                              volatile;
-                              curr; remains; params=bef; cst_l;
-                            }
-                        in
-                        whrec Cst_stack.empty (arg,cst_l :: app_sk')
-                  in
-                  let rec is_case x = match EConstr.kind sigma x with
-                    | Lambda (_,_, x) | LetIn (_,_,_, x) | Cast (x, _,_) -> is_case x
+                  let rec is_case x = match CbnClos.kind sigma x with
+                    | Lambda (_,_, x) | LetIn (_,_,_, x) -> is_case (CbnClos.liftn 1 x)
+                    | Cast (x, _,_) -> is_case x
                     | App (hd, _) -> is_case hd
                     | Case _ -> true
                     | _ -> false in
-                  if equal_stacks env sigma (x, app_sk) (tm', sk')
-                  || Stack.will_expose_iota sk'
-                  || is_case tm'
-                  then fold ()
-                  else whrec cst_l' (tm', sk' @ sk)
+                  let local_rel_is_unfoldable n =
+                    RedFlags.red_set flags RedFlags.fDELTA &&
+                    match lookup_rel n env with
+                    | LocalDef _ -> true
+                    | LocalAssum _ -> false
+                    | exception Not_found -> false
+                  in
+                  let local_var_is_unfoldable id =
+                    RedFlags.red_set flags (RedFlags.fVAR id) &&
+                    match lookup_named id env with
+                    | LocalDef _ -> true
+                    | LocalAssum _ -> false
+                    | exception Not_found -> false
+                  in
+                  (* Fast-path substitutions that are already stuck.  If the
+                     substituted value can still make head progress (local
+                     definitions, transparent constants, lets, beta-redexes,
+                     fixpoints, projections, ...), fall back to the ordinary
+                     weak-head pass below.  That pass is what notices that a
+                     [simpl nomatch] wrapper would expose a stuck case after
+                     zeta/delta/beta reduction and therefore refolds it. *)
+                  let rec is_obviously_stuck tm sk =
+                    not (Stack.will_expose_iota sk) &&
+                    match CbnClos.kind sigma tm with
+                    | Cast (tm, _, _) -> is_obviously_stuck tm sk
+                    | App (hd, args) -> is_obviously_stuck hd (Stack.append_app args sk)
+                    | Rel n -> not (local_rel_is_unfoldable n)
+                    | Var id -> not (local_var_is_unfoldable id)
+                    | Const (c, _) -> not (RedFlags.red_set flags (RedFlags.fCONST c))
+                    | Lambda _ -> Option.is_empty (Stack.decomp sk)
+                    | Construct _ | Ind _ | Evar _ | Meta _ | Sort _ | Prod _
+                    | Int _ | Float _ | String _ | Array _ -> true
+                    | LetIn _ | Case _ | Fix _ | CoFix _ | Proj _ -> false
+                  in
+                  let unfolds_to_subst_value = match recargs with
+                    | _ :: _ -> None
+                    | [] ->
+                      let cst_l' = Cst_stack.add_cst ~volatile ~refold_after_iota:true (mkConstU const) cst_l in
+                      let cst_l', (tm', sk') =
+                        apply_subst sigma cst_l' (CbnClos.inject body) app_sk in
+                      match CbnClos.subst_value sigma tm' with
+                      | Some tm' when is_obviously_stuck tm' sk' ->
+                        Some ((tm', sk'), cst_l')
+                      | Some _ | None -> None
+                  in
+                  begin match unfolds_to_subst_value with
+                  | Some ((tm', sk'), cst_l') -> whrec cst_l' (tm', sk' @ sk)
+                  | None ->
+                    let (tm',sk'),cst_l' =
+                      match recargs with
+                      | [] ->
+                        let cst_l = Cst_stack.add_cst ~volatile ~refold_after_iota:true
+                            (mkConstU const) cst_l in
+                        whrec cst_l (CbnClos.inject body, app_sk)
+                      | curr :: remains -> match Stack.strip_n_app curr app_sk with
+                        | None -> (x,app_sk), cst_l
+                        | Some (bef,arg,app_sk') ->
+                          let cst_l = Stack.Cst
+                              { const = Stack.Cst_const (fst const, u');
+                                volatile;
+                                refold_after_iota = true;
+                                curr; remains; params=bef; cst_l;
+                              }
+                          in
+                          whrec Cst_stack.empty (arg,cst_l :: app_sk')
+                    in
+                    (* If the selected recursive argument definitely changed,
+                       the unfolded state cannot be equal to the original one;
+                       avoid a full stack comparison, which may force unrelated
+                       arguments only to discard the equality result. *)
+                    let recarg_changed = match recargs with
+                      | [] -> false
+                      | curr :: _ ->
+                        not (CbnClos.equal sigma x tm') ||
+                        match Stack.strip_n_app curr app_sk, Stack.strip_n_app curr sk' with
+                        | Some (_, arg, _), Some (_, arg', _) ->
+                          not (CbnClos.equal sigma arg arg')
+                        | _ -> false
+                    in
+                    if (not recarg_changed && equal_stacks env sigma (x, app_sk) (tm', sk'))
+                    || Stack.will_expose_iota sk'
+                    || is_case tm'
+                    then fold ()
+                    else whrec cst_l' (tm', sk' @ sk)
+                  end
               | UnfoldWhen { recargs; nargs } -> (* maybe unfolds *)
                 begin match recargs with
                   | [] -> (* if nargs has been specified *)
                     (* CAUTION : the constant is NEVER refolded (even when it hides a (co)fix) *)
-                    whrec cst_l (body, stack)
+                    whrec cst_l (CbnClos.inject body, stack)
                   | curr :: remains -> match Stack.strip_n_app curr stack with
                     | None -> fold ()
                     | Some (bef,arg,s') ->
                       let cst_l = Stack.Cst
                           { const = Stack.Cst_const (fst const, u');
                             volatile = Option.has_some nargs;
+                            refold_after_iota = false;
                             curr; remains; params=bef; cst_l;
                           }
                       in
@@ -785,7 +1269,7 @@ let whd_state_gen ?csts flags env sigma =
             if not b then fold () else
             match Stack.strip_app stack with
             | args, (Stack.Fix (f,s',cst_l)::s'') when RedFlags.red_set flags RedFlags.fFIX ->
-                let x' = Stack.zip sigma (x, args) in
+                let x' = clos_of_app_stack sigma x args in
                 let out_sk = s' @ (Stack.append_app [|x'|] s'') in
                 reduce_and_refold_fix whrec env sigma cst_l f out_sk
             | _ -> fold ()
@@ -831,6 +1315,10 @@ let whd_state_gen ?csts flags env sigma =
                          curr;
                          remains;
                          volatile;
+                         refold_after_iota =
+                           (match behavior with
+                            | UnfoldWhenNoMatch _ -> true
+                            | UnfoldWhen _ | NeverUnfold -> false);
                          params=bef;
                          cst_l;
                        }
@@ -839,8 +1327,7 @@ let whd_state_gen ?csts flags env sigma =
            end)
 
     | LetIn (_,b,_,c) when RedFlags.red_set flags RedFlags.fZETA ->
-      let (cst_l, p) = apply_subst [b] sigma cst_l c stack in
-      whrec cst_l p
+      whrec cst_l (CbnClos.subst_cons b c, stack)
     | Cast (c,_,_) -> whrec cst_l (c, stack)
     | App (f,cl)  ->
       whrec
@@ -849,7 +1336,7 @@ let whd_state_gen ?csts flags env sigma =
     | Lambda (na,t,c) ->
       (match Stack.decomp stack with
       | Some _ when RedFlags.red_set flags RedFlags.fBETA ->
-        let (cst_l, p) = apply_subst [] sigma cst_l x stack in
+        let (cst_l, p) = apply_subst sigma cst_l x stack in
         whrec cst_l p
       | _ -> fold ())
 
@@ -867,17 +1354,40 @@ let whd_state_gen ?csts flags env sigma =
       let use_fix = RedFlags.red_set flags RedFlags.fFIX in
       if use_match || use_fix then
         match Stack.strip_app stack with
-        |args, (Stack.Case(case,_)::s') when use_match ->
+        |args, (Stack.Case(case,case_cst_l)::s') when use_match ->
           let r = apply_branch env sigma cstr args case in
-          whrec Cst_stack.empty (r, s')
+          let rec is_case x = match CbnClos.kind sigma x with
+            | Lambda (_,_, x) | LetIn (_,_,_, x) -> is_case (CbnClos.liftn 1 x)
+            | Cast (x, _,_) -> is_case x
+            | App (hd, _) -> is_case hd
+            | Case _ -> true
+            | _ -> false
+          in
+          let reduce_with_elim_csts cst_l p =
+            match cst_l, case_cst_l with
+            | [], _ :: _ when Cst_stack.may_refold_alias_after_iota case_cst_l && is_case r ->
+              (* [simpl nomatch] wrappers, including projection wrappers using
+                 [UnfoldWhenNoMatch], must stay folded when reducing under them
+                 exposes a stuck eliminator.  Do not do this for ordinary
+                 transparent aliases, even when the alias result has pending
+                 eliminations: after a real iota step master keeps the progress
+                 and reduces aliases such as [fst_nat] and [id_fun] away. *)
+              let (_, cst_l') as res = whrec case_cst_l p in
+              begin match cst_l' with
+              | [] -> res
+              | _ :: _ -> whrec Cst_stack.empty p
+              end
+            | [], [] | [], _ :: _ | _ :: _, _ -> whrec Cst_stack.empty p
+          in
+          reduce_with_elim_csts cst_l (r, s')
         |args, (Stack.Proj (p,_,_)::s') when use_match ->
           whrec Cst_stack.empty (Stack.nth args (Projection.npars p + Projection.arg p), s')
         |args, (Stack.Fix (f,s',cst_l)::s'') when use_fix ->
-          let x' = Stack.zip sigma (x, args) in
+          let x' = clos_of_app_stack sigma x args in
           let out_sk = s' @ (Stack.append_app [|x'|] s'') in
           reduce_and_refold_fix whrec env sigma cst_l f out_sk
-        |args, (Stack.Cst {const;curr;remains;volatile;params=s';cst_l} :: s'') ->
-          let x' = Stack.zip sigma (x, args) in
+        |args, (Stack.Cst {const;curr;remains;volatile;refold_after_iota;params=s';cst_l} :: s'') ->
+          let x' = clos_of_app_stack sigma x args in
           begin match remains with
           | [] ->
             (match const with
@@ -887,8 +1397,8 @@ let whd_state_gen ?csts flags env sigma =
               | Some body ->
                 let const = (fst const, EInstance.make (snd const)) in
                 let body = EConstr.of_constr body in
-                let cst_l = Cst_stack.add_cst ~volatile (mkConstU const) cst_l in
-                whrec cst_l (body, s' @ (Stack.append_app [|x'|] s'')))
+                let cst_l = Cst_stack.add_cst ~volatile ~refold_after_iota (mkConstU const) cst_l in
+                whrec cst_l (CbnClos.inject body, s' @ (Stack.append_app [|x'|] s'')))
             | Stack.Cst_proj (p,r) ->
               let stack = s' @ (Stack.append_app [|x'|] s'') in
               match Stack.strip_n_app 0 stack with
@@ -902,6 +1412,7 @@ let whd_state_gen ?csts flags env sigma =
                   { const;
                     curr=next;
                     volatile;
+                    refold_after_iota;
                     remains=remains';
                     params=s' @ (Stack.append_app [|x'|] bef);
                     cst_l;
@@ -922,29 +1433,12 @@ let whd_state_gen ?csts flags env sigma =
       else fold ()
 
     | Int _ | Float _ | String _ | Array _ ->
+      begin match reduce_primitive_value () with
+      | Some res -> res
+      | None ->
       begin match Stack.strip_app stack with
-       | (_, Stack.Primitive(p,(_,u as kn),rargs,kargs,cst_l')::s) ->
-         let more_to_reduce = List.exists (fun k -> CPrimitives.Kwhnf = k) kargs in
-         if more_to_reduce then
-           let (kargs,o) = Stack.get_next_primitive_args kargs s in
-           (* Should not fail because Primitive is put on the stack only if fully applied *)
-           let (before,a,after) = Option.get o in
-           whrec Cst_stack.empty (a,Stack.Primitive(p,kn,rargs @ Stack.append_app [|x|] before,kargs,cst_l')::after)
-         else
-           let n = List.length kargs in
-           let (args,s) = Stack.strip_app s in
-           let (args,extra_args) =
-             try List.chop n args
-             with List.IndexOutOfRange -> (args,[]) (* FIXME probably useless *)
-           in
-           let s = extra_args @ s in
-           let args = Array.of_list (Option.get (Stack.list_of_app_stack (rargs @ Stack.append_app [|x|] args))) in
-             begin match CredNative.red_prim env sigma p u args with
-               | Some t -> whrec cst_l' (t,s)
-               | None -> ((mkApp (mkConstU kn, args), s), cst_l)
-             end
-        |args, (Stack.Cst {const;curr;remains;volatile;params=s';cst_l} :: s'') ->
-          let x' = Stack.zip sigma (x, args) in
+        |args, (Stack.Cst {const;curr;remains;volatile;refold_after_iota;params=s';cst_l} :: s'') ->
+          let x' = clos_of_app_stack sigma x args in
           begin match remains with
           | [] ->
             (match const with
@@ -954,8 +1448,8 @@ let whd_state_gen ?csts flags env sigma =
               | Some body ->
                 let const = (fst const, EInstance.make (snd const)) in
                 let body = EConstr.of_constr body in
-                let cst_l = Cst_stack.add_cst ~volatile (mkConstU const) cst_l in
-                whrec cst_l (body, s' @ (Stack.append_app [|x'|] s'')))
+                let cst_l = Cst_stack.add_cst ~volatile ~refold_after_iota (mkConstU const) cst_l in
+                whrec cst_l (CbnClos.inject body, s' @ (Stack.append_app [|x'|] s'')))
             | Stack.Cst_proj (p,r) ->
               let stack = s' @ (Stack.append_app [|x'|] s'') in
               match Stack.strip_n_app 0 stack with
@@ -969,6 +1463,7 @@ let whd_state_gen ?csts flags env sigma =
                   { const;
                     curr=next;
                     volatile;
+                    refold_after_iota;
                     remains=remains';
                     params=s' @ (Stack.append_app [|x'|] bef);
                     cst_l;
@@ -978,26 +1473,32 @@ let whd_state_gen ?csts flags env sigma =
           end
        | _ -> fold ()
       end
+      end
 
     | Rel _ | Var _ | LetIn _ | Proj _ -> fold ()
     | Sort _ | Ind _ | Prod _ -> fold ()
   in
   fun xs ->
-  let (s,cst_l as res) = whrec (Option.default Cst_stack.empty csts) xs in
-  (Stack.best_state sigma s cst_l)
+  let (s,cst_l) = whrec (Option.default Cst_stack.empty csts) xs in
+  Stack.best_state ~inject:CbnClos.inject ~equal:(CbnClos.equal sigma) s cst_l
 
 let whd_cbn flags env sigma t =
-  let state = whd_state_gen flags env sigma (t, Stack.empty) in
-  Stack.zip ~refold:true sigma state
+  let state = whd_state_gen flags env sigma (CbnClos.inject t, Stack.empty) in
+  stack_zip ~refold:true sigma state
 
 let norm_cbn flags env sigma t =
   let push_rel_check_zeta d env =
     let open RedFlags in
     let d = match d with
-      | LocalDef (na,c,t) when not (red_set flags fZETA) -> LocalAssum (na,t)
+      | LocalDef (na,_,t) when not (red_set flags fZETA) -> LocalAssum (na,t)
       | d -> d in
-    push_rel d env in
+    push_rel d env
+  in
+  (* Refold the weak-head state before descending recursively.  If we map over
+     the delayed stack directly, application arguments are normalized before
+     enclosing case/fix/constant frames can refold or discard them. *)
   let rec strongrec env t =
-    map_constr_with_full_binders env sigma
-      push_rel_check_zeta strongrec env (whd_cbn flags env sigma t) in
+    Termops.map_constr_with_full_binders env sigma
+      push_rel_check_zeta strongrec env (whd_cbn flags env sigma t)
+  in
   strongrec env t
diff --git a/test-suite/output/cbn2.out b/test-suite/output/cbn2.out
new file mode 100644
index 000000000000..dae2c247d42d
--- /dev/null
+++ b/test-suite/output/cbn2.out
@@ -0,0 +1,26 @@
+File "./output/cbn2.v", line 80, characters 9-17:
+Warning: Use of "Notation" keyword for abbreviations is deprecated, use
+"Abbreviation" instead.
+[notation-for-abbreviation,deprecated-since-9.2,deprecated,default]
+Quickfix:
+Replace File "./output/cbn2.v", line 80, characters 9-17 with Abbreviation
+File "./output/cbn2.v", line 108, characters 2-14:
+Warning: This interactive proof is not started by the "Proof" command.
+[missing-proof-command,fragile,default]
+Quickfix:
+Replace File "./output/cbn2.v", line 108, characters 2-2 with Proof.
+
+File "./output/cbn2.v", line 109, characters 2-6:
+Warning: This interactive proof is not started by the "Proof" command.
+[missing-proof-command,fragile,default]
+Quickfix:
+Replace File "./output/cbn2.v", line 109, characters 2-2 with Proof.
+
+     = fun _ _ _ _ _ _ _ _ _ _ : nat => 8
+     : build_tele 10 -pt> nat
+     = fun _ _ _ _ _ _ _ _ _ _ : nat => 8
+     : build_tele 10 -pt> nat
+     = fun _ _ _ _ _ _ _ _ _ _ : nat => 2000
+     : build_tele 10 -pt> nat
+     = fun _ _ _ _ _ _ _ _ _ _ : nat => 2000
+     : build_tele 10 -pt> nat
diff --git a/test-suite/output/cbn2.v b/test-suite/output/cbn2.v
new file mode 100644
index 000000000000..9943abddf21e
--- /dev/null
+++ b/test-suite/output/cbn2.v
@@ -0,0 +1,263 @@
+(* motivating example *)
+Inductive type : Set :=
+    Tptr : type -> type
+  | Tref : type -> type
+  | Trv_ref : type -> type
+  | Tint : type -> type -> type
+  | Tvoid : type
+  | Tarray : type -> type -> type
+  | Tnamed : type -> type
+  | Tfunction : type -> type -> type -> type
+  | Tbool : type
+  | Tmember_pointer : type -> type -> type
+  | Tfloat : type -> type
+  | Tqualified : type -> type -> type
+  | Tnullptr : type
+  | Tnullptr1 : type
+  | Tnullptr2 : type
+  | Tnullptr3 : type
+  | Tnullptr4 : type
+  | Tnullptr5 : type
+  | Tnullptr6 : type
+  | Tnullptr7 : type
+  | Tnullptr8 : type
+  | Tnullptr9 : type
+  | Tnullptr10 : type
+  | Tnullptr11 : type
+  | Tnullptr12 : type
+  | Tnullptr13 : type
+  | Tnullptr14 : type
+  | Tnullptr15 : type
+  | Tnullptr16 : type
+  | Tnullptr17 : type
+  | Tnullptr18 : type
+  | Tnullptr19 : type
+  | tnullptr20 : type
+  | tnullptr21 : type
+  | tnullptr22 : type
+  | tnullptr23 : type
+  | tnullptr24 : type
+  | tnullptr25 : type
+  | tnullptr26 : type
+  | tnullptr27 : type
+  | tnullptr28 : type
+  | tnullptr29 : type
+  | tnullptr30 : type
+  | tnullptr31 : type
+  | tnullptr32 : type
+  | tnullptr33 : type
+  | tnullptr34 : type
+  | tnullptr35 : type
+  | tnullptr36 : type
+  | tnullptr37 : type
+  | tnullptr38 : type
+  | tnullptr39 : type
+  | Tarch : type -> type -> type
+  | Tbla : bla -> type
+  | Tblu : blu -> type
+  | Tbli : bli -> type
+with bla :=
+| bla1 : type -> bla
+| bla2 : type -> bla
+| bla3 : type -> bla
+| bla4 : type -> bla
+| bla5 : type -> bla
+with blu :=
+| blu1 : type -> blu
+| blu2 : type -> blu
+| blu3 : type -> blu
+| blu4 : type -> blu
+| blu5 : type -> blu
+with bli :=
+| bli1 : type -> bli
+| bli2 : type -> bli
+| bli3 : type -> bli
+| bli4 : type -> bli
+| bli5 : type -> bli
+.
+
+
+#[local] Notation EQ_DEC T := (forall x y : T, {x = y} + {~ x = y}) (only parsing).
+
+Lemma type_eq_dec' : EQ_DEC type
+with bla_eq_dec' : EQ_DEC bla
+with blu_eq_dec' : EQ_DEC blu
+with bli_eq_dec' : EQ_DEC bli.
+Proof.
+  all: intros x y.
+  all: pose (type_eq_dec' : EQ_DEC type).
+  all: pose (bla_eq_dec' : EQ_DEC bla).
+  all: pose (blu_eq_dec' : EQ_DEC blu).
+  all: pose (bli_eq_dec' : EQ_DEC bli).
+  all: decide equality.
+Defined.
+
+Definition type_eq_dec := Eval lazy zeta delta [type_eq_dec'] in type_eq_dec'.
+Definition bla_eq_dec :=  Eval lazy zeta delta [bla_eq_dec']  in bla_eq_dec'.
+Definition blu_eq_dec :=  Eval lazy zeta delta [blu_eq_dec']  in blu_eq_dec'.
+Definition bli_eq_dec :=  Eval lazy zeta delta [bli_eq_dec']  in bli_eq_dec'.
+
+Definition Decision := fun P : Prop => {P} + {~ P}.
+Definition RelDecision := fun {A B : Type} (R : A -> B -> Prop) => forall (x : A) (y : B), Decision (R x y).
+Definition bool_decide {P:Prop} : {P} + {~P} -> bool :=
+    fun x => match x with | left _ => true | right _ => false end.
+Definition decide_rel {A B : Type} (R : A -> B -> Prop) (RelDecision : RelDecision R) : forall (x : A) (y : B), Decision (R x y) :=
+  RelDecision.
+
+Goal (if if bool_decide (decide_rel _ type_eq_dec (Tarch Tvoid Tvoid) (Tarch Tvoid Tvoid)) then true else false then True else False).
+  Succeed cbn.
+  cbn.        (* Tactic call cbn   ran for 0.707 secs (0.706u,0.s) (su *)
+Abort.
+
+(* issue #18619 *)
+Fixpoint test (n : nat) (b : bool) :=
+  match n with
+  | 0 => if b then true else false
+  | S n => test n b
+  end.
+Arguments test : simpl nomatch.
+Goal forall b, test 5000 b = b.
+Proof. intros.
+  Succeed cbn.
+  assert_succeeds ((cbn);   lazymatch goal with |- test 0 b = b => idtac end). (* 3s *)
+Abort.
+
+(* issue #15720 *)
+Module Import PTELE.
+  Inductive tele : Type :=
+  | tO : tele
+  | tS {X : Type} : (X -> tele) -> tele.
+
+  Fixpoint tele_fun (t : tele) (T: Type) : Type :=
+    match t with
+    | tO => T
+    | tS F => forall x, tele_fun (F x) T
+    end.
+  Notation "t -pt> T" := (tele_fun t T)(format "t  -pt>  T", at level 99, T at level 200, right associativity).
+
+  Module FixArgs.
+  Section ArgRecord.
+    #[local] Set Primitive Projections.
+    Context {A : Type} {P : A -> Type}.
+    Record arg := taS' { arg_hd : A; arg_tl : P arg_hd }.
+  End ArgRecord.
+
+  Record argO := taO {}.
+  Arguments arg {_} _.
+
+  (* Eeverything below is identical to code in [FixArgsNonPrim] *)
+  Fixpoint tele_arg (t : tele) : Type :=
+    match t return Type with
+    | tO => argO
+    | tS F => arg (fun x => tele_arg (F x))
+    end.
+  Definition taS {X F} (x : X) (a : tele_arg (F x)) : tele_arg (tS F) :=
+    taS' x a.
+
+  Fixpoint tele_app {t : tele} {T} : tele_fun t T -> tele_arg t -> T :=
+    match t with
+    | tO => fun f _ => f
+    | tS F => fun f '(taS' x args) => tele_app (f x) args
+    end.
+  #[global] Arguments tele_app {!_ _} _ !_ /.
+
+  Fixpoint tele_bind {t:tele} {T} : (tele_arg t -> T) -> t -pt> T :=
+    match t with
+    | tO => fun g => g taO
+    | tS F => fun g x => tele_bind (fun a => g (taS x a))
+    end.
+  #[global] Arguments tele_bind {!_ _} _ /.
+
+  End FixArgs.
+
+  Module FixArgsNonPrim.
+
+  Section ArgRecord.
+    #[local] Unset Primitive Projections.
+    Context {A : Type} {P : A -> Type}.
+    Record arg := taS' { arg_hd : A; arg_tl : P arg_hd }.
+  End ArgRecord.
+
+  Record argO := taO {}.
+  Arguments arg {_} _.
+
+  (* Eeverything below is identical to code in [FixArgs] *)
+  Fixpoint tele_arg (t : tele) : Type :=
+    match t return Type with
+    | tO => argO
+    | tS F => arg (fun x => tele_arg (F x))
+    end.
+  Definition taS {X F} (x : X) (a : tele_arg (F x)) : tele_arg (tS F) :=
+    taS' x a.
+  #[global] Arguments taS _ _ _ & _.
+  Coercion tele_arg : tele >-> Sortclass.
+
+  Fixpoint tele_app {t : tele} {T} : tele_fun t T -> tele_arg t -> T :=
+    match t with
+    | tO => fun f _ => f
+    | tS F => fun f '(taS' x args) => tele_app (f x) args
+    end.
+  #[global] Arguments tele_app {!_ _} _ !_ /.
+
+  (** Currying telescopic functions *)
+  Fixpoint tele_bind {t:tele} {T} : (t -> T) -> t -pt> T :=
+    match t with
+    | tO => fun g => g taO
+    | tS F => fun g x => tele_bind (fun a => g (taS x a))
+    end.
+  #[global] Arguments tele_bind {!_ _} _ /.
+
+  End FixArgsNonPrim.
+
+End PTELE.
+
+Fixpoint build_tele (n : nat) : tele :=
+  match n with
+  | 0 => tO
+  | S n => tS (fun _ : nat => build_tele n)
+  end.
+
+Module Prim.
+  Import PTELE.FixArgs.
+  Fixpoint build_fn (n : nat) : build_tele n -pt> nat :=
+    match n as n return build_tele n -pt> nat with
+    | 0 => 0
+    | S n => fun x => build_fn n
+    end.
+
+  Fixpoint add (m n : nat) (p : build_tele n -pt> nat) : build_tele n -pt> nat :=
+    match m with
+    | 0 => p
+    | S m => tele_bind (fun x => 1 + tele_app (add m n p) x)
+    end.
+
+  Succeed Eval cbn in @add 8    10 (build_fn 10).
+  Eval cbn     in @add 8    10 (build_fn 10). (* 2.400s *)
+  (* Time Eval cbn     in @add 10   10 (build_fn 10). (* 11s    *) *)
+  (* [m=20] runs out of memory after a while. *)
+End Prim.
+
+Module NonPrim.
+  Import PTELE.FixArgsNonPrim.
+  Fixpoint build_fn (n : nat) : build_tele n -pt> nat :=
+    match n as n return build_tele n -pt> nat with
+    | 0 => 0
+    | S n => fun x => build_fn n
+    end.
+
+  Fixpoint add (m n : nat) (p : build_tele n -pt> nat) : build_tele n -pt> nat :=
+    match m with
+    | 0 => p
+    | S m => tele_bind (fun x => 1 + tele_app (add m n p) x)
+    end.
+
+  (* Time Eval cbn     in @add 2    10 (build_fn 10). (* 0.001s *) *)
+  (* Time Eval cbn     in @add 4    10 (build_fn 10). (* 0.003s *) *)
+  (* Time Eval cbn     in @add 8    10 (build_fn 10). (* 0.006s *) *)
+  (* Time Eval cbn     in @add 10   10 (build_fn 10). (* 0.008s *) *)
+  (* Time Eval cbn     in @add 20   10 (build_fn 10). (* 0.016s *) *)
+  (* Time Eval cbn     in @add 200  10 (build_fn 10). (* 0.17s  *) *)
+
+  Succeed Eval cbn in @add 2000 10 (build_fn 10).
+  Eval cbn     in @add 2000 10 (build_fn 10). (* 3.5s   *)
+End NonPrim.
diff --git a/test-suite/output/cbn_local_refolding.out b/test-suite/output/cbn_local_refolding.out
new file mode 100644
index 000000000000..31ffd300dfbe
--- /dev/null
+++ b/test-suite/output/cbn_local_refolding.out
@@ -0,0 +1,179 @@
+"id: let match arg"
+     : string
+     = fun x : nat => id match x with
+                         | 0 => 0
+                         | S p => p
+                         end
+     : nat -> nat
+"id: let pcase arg"
+     : string
+     = fun x : nat => id (pcase x)
+     : nat -> nat
+"id: let-bound function"
+     : string
+     = fun x : nat => id match x with
+                         | 0 => 0
+                         | S p => p
+                         end
+     : nat -> nat
+"fst: let match arg"
+     : string
+     = fun x : nat => fstn match x with
+                           | 0 => 0
+                           | S p => p
+                           end 0
+     : nat -> nat
+"snd: let match arg"
+     : string
+     = fun x : nat => sndn 0 match x with
+                             | 0 => 0
+                             | S p => p
+                             end
+     : nat -> nat
+"id: proof local function"
+     : string
+     = id (local_pcase x)
+     : nat
+"id: section let function"
+     : string
+     = fun x : nat => id (sec_pcase x)
+     : nat -> nat
+"def: let dictionary"
+     : string
+     = fun x : nat => difference dnat x 1
+     : nat -> nat
+"def: let open arg"
+     : string
+     = fun x : nat => difference dnat x 1
+     : nat -> nat
+"def: let beta open arg"
+     : string
+     = fun x : nat => difference dnat x 1
+     : nat -> nat
+"def: nested let dictionary and arg"
+     : string
+     = fun x : nat => difference dnat x 1
+     : nat -> nat
+"def: let wrapper"
+     : string
+     = fun x : nat => difference dnat x 1
+     : nat -> nat
+"def: let in dictionary body"
+     : string
+     = fun x : nat => difference dnat x 1
+     : nat -> nat
+"def: closed constructor control"
+     : string
+     = fun y : nat => y
+     : nat -> nat
+"class: let dictionary"
+     : string
+     = fun x : nat => difference dnat x 1
+     : nat -> nat
+"class: let open arg"
+     : string
+     = fun x : nat => difference dnat x 1
+     : nat -> nat
+"class: let beta open arg"
+     : string
+     = fun x : nat => difference dnat x 1
+     : nat -> nat
+"class: nested let dictionary and arg"
+     : string
+     = fun x : nat => difference dnat x 1
+     : nat -> nat
+"class: let wrapper"
+     : string
+     = fun x : nat => difference dnat x 1
+     : nat -> nat
+"class: let in dictionary body"
+     : string
+     = fun x : nat => difference dnat x 1
+     : nat -> nat
+"class: closed constructor control"
+     : string
+     = fun y : nat => y
+     : nat -> nat
+"set: let dictionary"
+     : string
+     = fun y : set => difference set_difference set0 y
+     : set -> set
+"set: let open second arg"
+     : string
+     = fun y : set => difference set_difference set0 y
+     : set -> set
+"set: let wrapper"
+     : string
+     = fun y : set => difference set_difference set0 y
+     : set -> set
+"set: closed constructor control"
+     : string
+     = exist (fun _ : nat => True) 0 I
+     : set
+"body: let around scrutinee"
+     : string
+     = fun x : nat => difference dlet_arg x 1
+     : nat -> nat
+"body: let in branch"
+     : string
+     = fun x : nat => difference dlet_branch x 1
+     : nat -> nat
+"body: dictionary constant is let"
+     : string
+     = fun x : nat => difference dlet_fun x 1
+     : nat -> nat
+"body: closed constructor control"
+     : string
+     = fun y : nat => y
+     : nat -> nat
+"proof local: dictionary"
+     : string
+     = difference D x 1
+     : nat
+"proof local: open arg"
+     : string
+     = difference dnat x' 1
+     : nat
+"proof local: wrapper"
+     : string
+     = f x 1
+     : nat
+"proof local: inline dictionary"
+     : string
+     = difference D x 1
+     : nat
+"proof local set: dictionary"
+     : string
+     = difference D set0 y
+     : set
+"proof local set: open arg"
+     : string
+     = difference set_difference set0 y'
+     : set
+"proof local set: wrapper"
+     : string
+     = f set0 y
+     : set
+"tactic: proof local dictionary"
+     : string
+1 goal
+  
+  x : nat
+  D := dnat : Difference nat
+  ============================
+  difference D x 1 = difference D x 1
+"tactic: term let dictionary"
+     : string
+1 goal
+  
+  x : nat
+  ============================
+  difference dnat x 1 = difference dnat x 1
+"tactic: proof local arg"
+     : string
+1 goal
+  
+  x : nat
+  x' := x : nat
+  ============================
+  difference dnat x' 1 = difference dnat x' 1
diff --git a/test-suite/output/cbn_local_refolding.v b/test-suite/output/cbn_local_refolding.v
new file mode 100644
index 000000000000..323fadba86dc
--- /dev/null
+++ b/test-suite/output/cbn_local_refolding.v
@@ -0,0 +1,269 @@
+(* Regression tests for cbn refolding with local definitions.
+   The expected output is the behavior of master: [simpl nomatch]
+   wrappers must remain folded when unfolding them would expose a stuck
+   match/let-pattern in head position, even when the wrapper, dictionary, or
+   arguments pass through local definitions. *)
+
+Set Printing Width 200.
+Require Import PrimString.
+Open Scope pstring_scope.
+
+Module IdentityLocalLets.
+  Definition id (n : nat) := n.
+  Definition fstn (x y : nat) := x.
+  Definition sndn (x y : nat) := y.
+  Definition pcase (n : nat) := match n with O => O | S p => p end.
+  Arguments id n / : simpl nomatch.
+  Arguments fstn x y / : simpl nomatch.
+  Arguments sndn x y / : simpl nomatch.
+
+  Check "id: let match arg".
+  Eval cbn in (fun x : nat => id (let y := match x with O => O | S p => p end in y)).
+
+  Check "id: let pcase arg".
+  Eval cbn in (fun x : nat => id (let y := pcase x in y)).
+
+  Check "id: let-bound function".
+  Eval cbn in (fun x : nat => let local_pcase := fun n : nat => match n with O => O | S p => p end in id (local_pcase x)).
+
+  Check "fst: let match arg".
+  Eval cbn in (fun x : nat => fstn (let y := match x with O => O | S p => p end in y) O).
+
+  Check "snd: let match arg".
+  Eval cbn in (fun x : nat => sndn O (let y := match x with O => O | S p => p end in y)).
+
+  Goal forall x : nat, True.
+  Proof.
+    intro x.
+    pose (local_pcase := fun n : nat => match n with O => O | S p => p end).
+    Check "id: proof local function".
+    Eval cbn in (id (local_pcase x)).
+    exact I.
+  Qed.
+End IdentityLocalLets.
+
+Module SectionLetLocalDefinition.
+  Definition id (n : nat) := n.
+  Arguments id n / : simpl nomatch.
+
+  Section S.
+    Let sec_pcase (n : nat) := match n with O => O | S p => p end.
+
+    Check "id: section let function".
+    Eval cbn in (fun x : nat => id (sec_pcase x)).
+  End S.
+End SectionLetLocalDefinition.
+
+Module DefClassLocalLets.
+  Definition Difference A := A -> A -> A.
+  Definition difference {A} {D : Difference A} : A -> A -> A := D.
+  Definition dnat : Difference nat := fun x y => match x with O => y | S z => z end.
+  Arguments difference {A} D / _ _ : simpl nomatch.
+
+  Check "def: let dictionary".
+  Eval cbn in (fun x : nat => let D := dnat in @difference nat D x (S O)).
+
+  Check "def: let open arg".
+  Eval cbn in (fun x : nat => let x' := x in @difference nat dnat x' (S O)).
+
+  Check "def: let beta open arg".
+  Eval cbn in (fun x : nat => let x' := (fun z : nat => z) x in @difference nat dnat x' (S O)).
+
+  Check "def: nested let dictionary and arg".
+  Eval cbn in (fun x : nat => let D := dnat in let x' := x in @difference nat D x' (S O)).
+
+  Check "def: let wrapper".
+  Eval cbn in (fun x : nat => let f := @difference nat dnat in f x (S O)).
+
+  Check "def: let in dictionary body".
+  Eval cbn in (fun x : nat => @difference nat (let D := dnat in D) x (S O)).
+
+  Check "def: closed constructor control".
+  Eval cbn in (fun y : nat => let x' := O in @difference nat dnat x' y).
+End DefClassLocalLets.
+
+Module ClassLocalLets.
+  Class Difference A := difference : A -> A -> A.
+  Definition dnat : Difference nat := fun x y => match x with O => y | S z => z end.
+  Arguments difference {A} Difference / _ _ : simpl nomatch.
+
+  Check "class: let dictionary".
+  Eval cbn in (fun x : nat => let D := dnat in @difference nat D x (S O)).
+
+  Check "class: let open arg".
+  Eval cbn in (fun x : nat => let x' := x in @difference nat dnat x' (S O)).
+
+  Check "class: let beta open arg".
+  Eval cbn in (fun x : nat => let x' := (fun z : nat => z) x in @difference nat dnat x' (S O)).
+
+  Check "class: nested let dictionary and arg".
+  Eval cbn in (fun x : nat => let D := dnat in let x' := x in @difference nat D x' (S O)).
+
+  Check "class: let wrapper".
+  Eval cbn in (fun x : nat => let f := @difference nat dnat in f x (S O)).
+
+  Check "class: let in dictionary body".
+  Eval cbn in (fun x : nat => @difference nat (let D := dnat in D) x (S O)).
+
+  Check "class: closed constructor control".
+  Eval cbn in (fun y : nat => let x' := O in @difference nat dnat x' y).
+End ClassLocalLets.
+
+Module SetLocalLets.
+  Definition Difference A := A -> A -> A.
+  Definition difference {A} {D : Difference A} : A -> A -> A := D.
+  Definition set := { t : nat | True }.
+  Definition set0 : set := exist _ O I.
+  Definition setS (n : nat) : set := exist _ (S n) I.
+  Definition set_difference : Difference set := fun X Y => let (t1, _) := X in let (t2, _) := Y in exist _ t1 I.
+  Arguments difference {A} D / _ _ : simpl nomatch.
+
+  Check "set: let dictionary".
+  Eval cbn in (fun y : set => let D := set_difference in @difference set D set0 y).
+
+  Check "set: let open second arg".
+  Eval cbn in (fun y : set => let y' := y in @difference set set_difference set0 y').
+
+  Check "set: let wrapper".
+  Eval cbn in (fun y : set => let f := @difference set set_difference in f set0 y).
+
+  Check "set: closed constructor control".
+  Eval cbn in (let D := set_difference in @difference set D set0 (setS O)).
+End SetLocalLets.
+
+Module DictionaryBodiesWithLets.
+  Definition Difference A := A -> A -> A.
+  Definition difference {A} {D : Difference A} : A -> A -> A := D.
+  Arguments difference {A} D / _ _ : simpl nomatch.
+
+  Definition dlet_arg : Difference nat := fun x y => let z := x in match z with O => y | S w => w end.
+  Definition dlet_branch : Difference nat := fun x y => match x with O => let z := y in z | S w => w end.
+  Definition dlet_fun : Difference nat := let D := fun x y => match x with O => y | S w => w end in D.
+
+  Check "body: let around scrutinee".
+  Eval cbn in (fun x : nat => @difference nat dlet_arg x (S O)).
+
+  Check "body: let in branch".
+  Eval cbn in (fun x : nat => @difference nat dlet_branch x (S O)).
+
+  Check "body: dictionary constant is let".
+  Eval cbn in (fun x : nat => @difference nat dlet_fun x (S O)).
+
+  Check "body: closed constructor control".
+  Eval cbn in (fun y : nat => @difference nat dlet_arg O y).
+End DictionaryBodiesWithLets.
+
+Module ProofLocalDefinitions.
+  Definition Difference A := A -> A -> A.
+  Definition difference {A} {D : Difference A} : A -> A -> A := D.
+  Definition dnat : Difference nat := fun x y => match x with O => y | S z => z end.
+  Arguments difference {A} D / _ _ : simpl nomatch.
+
+  Goal forall x : nat, True.
+  Proof.
+    intro x.
+    pose (D := dnat).
+    Check "proof local: dictionary".
+    Eval cbn in (@difference nat D x (S O)).
+    exact I.
+  Qed.
+
+  Goal forall x : nat, True.
+  Proof.
+    intro x.
+    pose (x' := x).
+    Check "proof local: open arg".
+    Eval cbn in (@difference nat dnat x' (S O)).
+    exact I.
+  Qed.
+
+  Goal forall x : nat, True.
+  Proof.
+    intro x.
+    pose (f := @difference nat dnat).
+    Check "proof local: wrapper".
+    Eval cbn in (f x (S O)).
+    exact I.
+  Qed.
+
+  Goal forall x : nat, True.
+  Proof.
+    intro x.
+    pose (D := fun a b : nat => match a with O => b | S z => z end).
+    Check "proof local: inline dictionary".
+    Eval cbn in (@difference nat D x (S O)).
+    exact I.
+  Qed.
+End ProofLocalDefinitions.
+
+Module ProofLocalSetDefinitions.
+  Definition Difference A := A -> A -> A.
+  Definition difference {A} {D : Difference A} : A -> A -> A := D.
+  Definition set := { t : nat | True }.
+  Definition set0 : set := exist _ O I.
+  Definition set_difference : Difference set := fun X Y => let (t1, _) := X in let (t2, _) := Y in exist _ t1 I.
+  Arguments difference {A} D / _ _ : simpl nomatch.
+
+  Goal forall y : set, True.
+  Proof.
+    intro y.
+    pose (D := set_difference).
+    Check "proof local set: dictionary".
+    Eval cbn in (@difference set D set0 y).
+    exact I.
+  Qed.
+
+  Goal forall y : set, True.
+  Proof.
+    intro y.
+    pose (y' := y).
+    Check "proof local set: open arg".
+    Eval cbn in (@difference set set_difference set0 y').
+    exact I.
+  Qed.
+
+  Goal forall y : set, True.
+  Proof.
+    intro y.
+    pose (f := @difference set set_difference).
+    Check "proof local set: wrapper".
+    Eval cbn in (f set0 y).
+    exact I.
+  Qed.
+End ProofLocalSetDefinitions.
+
+Module CbnTacticGoals.
+  Definition Difference A := A -> A -> A.
+  Definition difference {A} {D : Difference A} : A -> A -> A := D.
+  Definition dnat : Difference nat := fun x y => match x with O => y | S z => z end.
+  Arguments difference {A} D / _ _ : simpl nomatch.
+
+  Goal forall x : nat, True.
+  Proof.
+    intro x.
+    pose (D := dnat).
+    enough (@difference nat D x (S O) = @difference nat D x (S O)) by exact I.
+    Check "tactic: proof local dictionary".
+    cbn.
+    Show.
+  Abort.
+
+  Goal forall x : nat, True.
+  Proof.
+    intro x.
+    enough ((let D := dnat in @difference nat D x (S O)) = (let D := dnat in @difference nat D x (S O))) by exact I.
+    Check "tactic: term let dictionary".
+    cbn.
+    Show.
+  Abort.
+
+  Goal forall x : nat, True.
+  Proof.
+    intro x.
+    pose (x' := x).
+    enough (@difference nat dnat x' (S O) = @difference nat dnat x' (S O)) by exact I.
+    Check "tactic: proof local arg".
+    cbn.
+    Show.
+  Abort.
+End CbnTacticGoals.
diff --git a/test-suite/output/cbn_refolding.out b/test-suite/output/cbn_refolding.out
new file mode 100644
index 000000000000..c9ed49026e9d
--- /dev/null
+++ b/test-suite/output/cbn_refolding.out
@@ -0,0 +1,190 @@
+"** direct closed aliases"
+     : string
+     = 0
+     : nat
+     = 0
+     : nat
+     = exist (fun _ : nat => True) 0 I
+     : set
+"** aliases over reduced iota arguments"
+     : string
+"alias_id_nat_inline_match_S"
+     : string
+     = fun x : nat => x
+     : nat -> nat
+"alias_id_nat_inline_if_true"
+     : string
+     = fun x : nat => S x
+     : nat -> nat
+"alias_id_nat_def_match_S"
+     : string
+     = fun x : nat => x
+     : nat -> nat
+"alias_id_nat_def_match_SS"
+     : string
+     = fun x : nat => x
+     : nat -> nat
+"alias_id_nat_beta_then_iota"
+     : string
+     = fun x : nat => x
+     : nat -> nat
+"alias_fst_nat_inline_match_S"
+     : string
+     = fun x : nat => x
+     : nat -> nat
+"alias_fst_nat_inline_if_true"
+     : string
+     = fun x : nat => S x
+     : nat -> nat
+"alias_fst_nat_def_match_S"
+     : string
+     = fun x : nat => x
+     : nat -> nat
+"alias_fst_nat_def_match_SS"
+     : string
+     = fun x : nat => x
+     : nat -> nat
+"alias_fst_nat_beta_then_iota"
+     : string
+     = fun x : nat => x
+     : nat -> nat
+"alias_snd_nat_inline_match_S"
+     : string
+     = fun x : nat => x
+     : nat -> nat
+"alias_snd_nat_inline_if_true"
+     : string
+     = fun x : nat => S x
+     : nat -> nat
+"alias_snd_nat_def_match_S"
+     : string
+     = fun x : nat => x
+     : nat -> nat
+"alias_snd_nat_def_match_SS"
+     : string
+     = fun x : nat => x
+     : nat -> nat
+"alias_snd_nat_beta_then_iota"
+     : string
+     = fun x : nat => x
+     : nat -> nat
+"alias_third_nat_inline_match_S"
+     : string
+     = fun x : nat => x
+     : nat -> nat
+"alias_third_nat_inline_if_true"
+     : string
+     = fun x : nat => S x
+     : nat -> nat
+"alias_third_nat_def_match_S"
+     : string
+     = fun x : nat => x
+     : nat -> nat
+"alias_third_nat_def_match_SS"
+     : string
+     = fun x : nat => x
+     : nat -> nat
+"alias_third_nat_beta_then_iota"
+     : string
+     = fun x : nat => x
+     : nat -> nat
+"alias_id_poly_nat_inline_match_S"
+     : string
+     = fun x : nat => x
+     : nat -> nat
+"alias_id_poly_nat_inline_if_true"
+     : string
+     = fun x : nat => S x
+     : nat -> nat
+"alias_id_poly_nat_def_match_S"
+     : string
+     = fun x : nat => x
+     : nat -> nat
+"alias_id_poly_nat_def_match_SS"
+     : string
+     = fun x : nat => x
+     : nat -> nat
+"alias_id_poly_nat_beta_then_iota"
+     : string
+     = fun x : nat => x
+     : nat -> nat
+"alias_ret_cast_inline_match_S"
+     : string
+     = fun x : nat => x
+     : nat -> nat
+"alias_ret_cast_inline_if_true"
+     : string
+     = fun x : nat => S x
+     : nat -> nat
+"alias_ret_cast_def_match_S"
+     : string
+     = fun x : nat => x
+     : nat -> nat
+"alias_ret_cast_def_match_SS"
+     : string
+     = fun x : nat => x
+     : nat -> nat
+"alias_ret_cast_beta_then_iota"
+     : string
+     = fun x : nat => x
+     : nat -> nat
+"selected_under_pair"
+     : string
+     = fun x : nat => (x, 0)
+     : nat -> nat * nat
+"sort_id_Type_if_true"
+     : string
+     = nat
+     : Type
+"sort_id_Prop_if_true"
+     : string
+     = True
+     : Prop
+"sort_id_Prop_under_fun"
+     : string
+     = fun P : Prop => P
+     : Prop -> Prop
+"fun_id_if_true"
+     : string
+     = S
+     : nat -> nat
+"fun_id_if_true_applied"
+     : string
+     = fun x : nat => S x
+     : nat -> nat
+"record_id_R_if_true"
+     : string
+     = fun x : nat => {| ra := x; rb := 0 |}
+     : nat -> R
+"prim_record_id_PR_if_true"
+     : string
+     = fun x : nat => {| pra := x; prb := 0 |}
+     : nat -> PR
+"box_id_if_true"
+     : string
+     = Box 0
+     : box
+"set_id_poly_if_true"
+     : string
+     = set0
+     : set
+"set_difference_direct"
+     : string
+     = fun y : set => let (t2, _) := y in exist (fun _ : nat => True) 0 I
+     : set -> set
+"set_difference_cast"
+     : string
+     = fun y : set => let (t2, _) := y in exist (fun _ : nat => True) 0 I
+     : set -> set
+"set_difference_class"
+     : string
+     = fun y : set => let (t2, _) := y in exist (fun _ : nat => True) 0 I
+     : set -> set
+"set_difference_direct_both_known"
+     : string
+     = exist (fun _ : nat => True) 0 I
+     : set
+"set_difference_class_both_known"
+     : string
+     = exist (fun _ : nat => True) 0 I
+     : set
diff --git a/test-suite/output/cbn_refolding.v b/test-suite/output/cbn_refolding.v
new file mode 100644
index 000000000000..721a3e6125fd
--- /dev/null
+++ b/test-suite/output/cbn_refolding.v
@@ -0,0 +1,142 @@
+(* Regression tests for cbn refolding after iota.
+   The expected output is the behavior of master: transparent aliases
+   must not be refolded once their arguments have reduced enough to
+   allow the alias itself to compute. *)
+
+
+Set Printing Width 200.
+Require Import PrimString.
+Open Scope pstring_scope.
+
+Definition id_nat (x : nat) := x.
+Definition id_Type (A : Type) := A.
+Definition id_Prop (P : Prop) := P.
+Definition id_fun (f : nat -> nat) := f.
+Definition id_pair (p : nat * nat) := p.
+Definition fst_nat (x y : nat) := x.
+Definition snd_nat (x y : nat) := y.
+Definition third_nat (x y z : nat) := z.
+Definition id_poly {A : Type} (x : A) := x.
+Definition ret_cast (x : nat) : nat := (x : nat).
+
+Definition pcase (n : nat) := match n with O => O | S p => p end.
+Definition pcase2 (n : nat) := match n with O => O | S p => match p with O => O | S q => q end end.
+
+Inductive box := Box : nat -> box | Empty : box.
+Definition id_box (b : box) := b.
+
+Record R := mkR { ra : nat; rb : nat }.
+Definition id_R (r : R) := r.
+
+Set Primitive Projections.
+Record PR := mkPR { pra : nat; prb : nat }.
+Unset Primitive Projections.
+Definition id_PR (r : PR) := r.
+
+Definition set := { t : nat | True }.
+Definition set0 : set := exist _ O I.
+Definition setS (n : nat) : set := exist _ (S n) I.
+Definition set_difference : set -> set -> set :=
+  fun X Y => let (t1, _) := X in let (t2, _) := Y in exist _ t1 I.
+Definition difference_direct {A} (D : A -> A -> A) : A -> A -> A := D.
+Definition difference_cast {A} (D : A -> A -> A) : A -> A -> A := (D : A -> A -> A).
+
+Class Difference (A : Type) := difference_cls : A -> A -> A.
+Definition set_difference_cls : Difference set := set_difference.
+
+Check "** direct closed aliases".
+Eval cbn in id_nat (if true then O else S O).
+Eval cbn in id_nat (match S O with O => O | S p => p end).
+Eval cbn in @difference_cls set set_difference_cls set0 (setS O).
+
+Check "** aliases over reduced iota arguments".
+Check "alias_id_nat_inline_match_S".
+Eval cbn in (fun x : nat => id_nat ((match S x with O => O | S p => p end))).
+Check "alias_id_nat_inline_if_true".
+Eval cbn in (fun x : nat => id_nat ((if true then S x else O))).
+Check "alias_id_nat_def_match_S".
+Eval cbn in (fun x : nat => id_nat (pcase (S x))).
+Check "alias_id_nat_def_match_SS".
+Eval cbn in (fun x : nat => id_nat (pcase2 (S (S x)))).
+Check "alias_id_nat_beta_then_iota".
+Eval cbn in (fun x : nat => id_nat (((fun y : nat => pcase (S y)) x))).
+Check "alias_fst_nat_inline_match_S".
+Eval cbn in (fun x : nat => fst_nat ((match S x with O => O | S p => p end)) O).
+Check "alias_fst_nat_inline_if_true".
+Eval cbn in (fun x : nat => fst_nat ((if true then S x else O)) O).
+Check "alias_fst_nat_def_match_S".
+Eval cbn in (fun x : nat => fst_nat (pcase (S x)) O).
+Check "alias_fst_nat_def_match_SS".
+Eval cbn in (fun x : nat => fst_nat (pcase2 (S (S x))) O).
+Check "alias_fst_nat_beta_then_iota".
+Eval cbn in (fun x : nat => fst_nat (((fun y : nat => pcase (S y)) x)) O).
+Check "alias_snd_nat_inline_match_S".
+Eval cbn in (fun x : nat => snd_nat O ((match S x with O => O | S p => p end))).
+Check "alias_snd_nat_inline_if_true".
+Eval cbn in (fun x : nat => snd_nat O ((if true then S x else O))).
+Check "alias_snd_nat_def_match_S".
+Eval cbn in (fun x : nat => snd_nat O (pcase (S x))).
+Check "alias_snd_nat_def_match_SS".
+Eval cbn in (fun x : nat => snd_nat O (pcase2 (S (S x)))).
+Check "alias_snd_nat_beta_then_iota".
+Eval cbn in (fun x : nat => snd_nat O (((fun y : nat => pcase (S y)) x))).
+Check "alias_third_nat_inline_match_S".
+Eval cbn in (fun x : nat => third_nat O O ((match S x with O => O | S p => p end))).
+Check "alias_third_nat_inline_if_true".
+Eval cbn in (fun x : nat => third_nat O O ((if true then S x else O))).
+Check "alias_third_nat_def_match_S".
+Eval cbn in (fun x : nat => third_nat O O (pcase (S x))).
+Check "alias_third_nat_def_match_SS".
+Eval cbn in (fun x : nat => third_nat O O (pcase2 (S (S x)))).
+Check "alias_third_nat_beta_then_iota".
+Eval cbn in (fun x : nat => third_nat O O (((fun y : nat => pcase (S y)) x))).
+Check "alias_id_poly_nat_inline_match_S".
+Eval cbn in (fun x : nat => @id_poly nat ((match S x with O => O | S p => p end))).
+Check "alias_id_poly_nat_inline_if_true".
+Eval cbn in (fun x : nat => @id_poly nat ((if true then S x else O))).
+Check "alias_id_poly_nat_def_match_S".
+Eval cbn in (fun x : nat => @id_poly nat (pcase (S x))).
+Check "alias_id_poly_nat_def_match_SS".
+Eval cbn in (fun x : nat => @id_poly nat (pcase2 (S (S x)))).
+Check "alias_id_poly_nat_beta_then_iota".
+Eval cbn in (fun x : nat => @id_poly nat (((fun y : nat => pcase (S y)) x))).
+Check "alias_ret_cast_inline_match_S".
+Eval cbn in (fun x : nat => ret_cast ((match S x with O => O | S p => p end))).
+Check "alias_ret_cast_inline_if_true".
+Eval cbn in (fun x : nat => ret_cast ((if true then S x else O))).
+Check "alias_ret_cast_def_match_S".
+Eval cbn in (fun x : nat => ret_cast (pcase (S x))).
+Check "alias_ret_cast_def_match_SS".
+Eval cbn in (fun x : nat => ret_cast (pcase2 (S (S x)))).
+Check "alias_ret_cast_beta_then_iota".
+Eval cbn in (fun x : nat => ret_cast (((fun y : nat => pcase (S y)) x))).
+Check "selected_under_pair".
+Eval cbn in (fun x : nat => id_pair (match true with true => (x,O) | false => (O,x) end)).
+Check "sort_id_Type_if_true".
+Eval cbn in id_Type (if true then nat else bool).
+Check "sort_id_Prop_if_true".
+Eval cbn in id_Prop (if true then True else False).
+Check "sort_id_Prop_under_fun".
+Eval cbn in (fun P : Prop => id_Prop (if true then P else False)).
+Check "fun_id_if_true".
+Eval cbn in id_fun (if true then S else fun x => x).
+Check "fun_id_if_true_applied".
+Eval cbn in (fun x : nat => id_fun (if true then S else fun x => x) x).
+Check "record_id_R_if_true".
+Eval cbn in (fun x : nat => id_R (if true then mkR x O else mkR O x)).
+Check "prim_record_id_PR_if_true".
+Eval cbn in (fun x : nat => id_PR (if true then mkPR x O else mkPR O x)).
+Check "box_id_if_true".
+Eval cbn in id_box (if true then Box O else Empty).
+Check "set_id_poly_if_true".
+Eval cbn in @id_poly set (if true then set0 else setS O).
+Check "set_difference_direct".
+Eval cbn in (fun y : set => @difference_direct set set_difference set0 y).
+Check "set_difference_cast".
+Eval cbn in (fun y : set => @difference_cast set set_difference set0 y).
+Check "set_difference_class".
+Eval cbn in (fun y : set => @difference_cls set set_difference_cls set0 y).
+Check "set_difference_direct_both_known".
+Eval cbn in @difference_direct set set_difference set0 (setS O).
+Check "set_difference_class_both_known".
+Eval cbn in @difference_cls set set_difference_cls set0 (setS O).
diff --git a/test-suite/success/cbn.v b/test-suite/success/cbn.v
index 02a0a6264790..4ab8784dc72b 100644
--- a/test-suite/success/cbn.v
+++ b/test-suite/success/cbn.v
@@ -71,3 +71,98 @@ match goal with [ |- (n, scons n (mut_stream2 x (n + x))) = (n, scons n (mut_str
 Abort.
 
 End MutualFixCoFixInSection.
+
+Module RefoldProjectionAlias.
+
+Module AsClass.
+  Class Difference A := difference : A -> A -> A.
+  Definition set := { t : nat | True }.
+  Definition set_difference : Difference set := fun X Y =>
+    let (t1, _) := X in let (t2, _) := Y in exist _ t1 I.
+
+  Goal forall y : set, True.
+  Proof.
+    intro y.
+    let v := eval cbn in (@difference set set_difference (exist _ 0 I) y) in
+    lazymatch v with
+    | difference (exist _ 0 I) y => exact I
+    | _ => fail "difference was not refolded"
+    end.
+  Qed.
+End AsClass.
+
+Module AsDef.
+  Definition Difference A := A -> A -> A.
+  Definition difference {A} {D : Difference A} : A -> A -> A := D.
+  Definition set := { t : nat | True }.
+  Definition set_difference : Difference set := fun X Y =>
+    let (t1, _) := X in let (t2, _) := Y in exist _ t1 I.
+
+  Goal forall y : set, True.
+  Proof.
+    intro y.
+    let v := eval cbn in (@difference set set_difference (exist _ 0 I) y) in
+    lazymatch v with
+    | difference (exist _ 0 I) y => exact I
+    | _ => fail "difference was not refolded"
+    end.
+  Qed.
+End AsDef.
+
+End RefoldProjectionAlias.
+
+Module RefoldAfterPositiveIota.
+
+Inductive tree (A : Type) :=
+| Leaf : tree A
+| Node : tree A -> A -> tree A -> tree A.
+Arguments Leaf {A}.
+Arguments Node {A} _ _ _.
+
+Definition bal {A} (l : tree A) (x : A) (r : tree A) := Node l x r.
+
+Fixpoint remove_min {A} (l : tree A) (x : A) (r : tree A) : tree A * A :=
+  match l with
+  | Leaf => (r, x)
+  | Node ll lx lr =>
+    let (l', m) := remove_min ll lx lr in
+    (bal l' x r, m)
+  end.
+
+Definition merge {A} (s1 s2 : tree A) :=
+  match s1, s2 with
+  | Leaf, _ => s2
+  | _, Leaf => s1
+  | _, Node l2 x2 r2 =>
+    match remove_min l2 x2 r2 with
+    | (s2', x) => bal s1 x s2'
+    end
+  end.
+
+#[local] Ltac caseq :=
+match goal with [ |- context [match ?t with _ => _ end] ] =>
+  let cmp := fresh in
+  let H := fresh in
+  remember t as cmp eqn:H; symmetry in H; destruct cmp
+end.
+
+(* The [Node] branch of [merge] exposes a stuck match on the second tree.
+   [cbn] must not refold [merge] after making the positive iota step on the
+   first tree; otherwise this induction principle is left with open goals. *)
+Lemma merge_ind {A : Type} {P : tree A -> tree A -> tree A -> Prop} :
+  (forall s1 s2 : tree A, s1 = Leaf -> P Leaf s2 s2) ->
+  (forall (s1 s2 l1 : tree A) (x1 : A) (r1 : tree A),
+   s1 = Node l1 x1 r1 -> s2 = Leaf -> P (Node l1 x1 r1) Leaf s1) ->
+  (forall (s1 s2 l1 : tree A) (x1 : A) (r1 : tree A),
+   s1 = Node l1 x1 r1 ->
+   forall (l2 : tree A) (x2 : A) (r2 : tree A),
+   s2 = Node l2 x2 r2 ->
+   forall (s2' : tree A) (x : A),
+   remove_min l2 x2 r2 = (s2', x) ->
+   P (Node l1 x1 r1) (Node l2 x2 r2) (bal s1 x s2')) ->
+  forall s1 s2 : tree A, P s1 s2 (merge s1 s2).
+Proof.
+intros; induction s1; cbn; repeat caseq; eauto.
+Qed.
+
+End RefoldAfterPositiveIota.
diff --git a/test-suite/success/cbn2.v b/test-suite/success/cbn2.v
new file mode 100644
index 000000000000..31ef83d61b99
--- /dev/null
+++ b/test-suite/success/cbn2.v
@@ -0,0 +1,263 @@
+(* motivating example *)
+Inductive type : Set :=
+    Tptr : type -> type
+  | Tref : type -> type
+  | Trv_ref : type -> type
+  | Tint : type -> type -> type
+  | Tvoid : type
+  | Tarray : type -> type -> type
+  | Tnamed : type -> type
+  | Tfunction : type -> type -> type -> type
+  | Tbool : type
+  | Tmember_pointer : type -> type -> type
+  | Tfloat : type -> type
+  | Tqualified : type -> type -> type
+  | Tnullptr : type
+  | Tnullptr1 : type
+  | Tnullptr2 : type
+  | Tnullptr3 : type
+  | Tnullptr4 : type
+  | Tnullptr5 : type
+  | Tnullptr6 : type
+  | Tnullptr7 : type
+  | Tnullptr8 : type
+  | Tnullptr9 : type
+  | Tnullptr10 : type
+  | Tnullptr11 : type
+  | Tnullptr12 : type
+  | Tnullptr13 : type
+  | Tnullptr14 : type
+  | Tnullptr15 : type
+  | Tnullptr16 : type
+  | Tnullptr17 : type
+  | Tnullptr18 : type
+  | Tnullptr19 : type
+  | tnullptr20 : type
+  | tnullptr21 : type
+  | tnullptr22 : type
+  | tnullptr23 : type
+  | tnullptr24 : type
+  | tnullptr25 : type
+  | tnullptr26 : type
+  | tnullptr27 : type
+  | tnullptr28 : type
+  | tnullptr29 : type
+  | tnullptr30 : type
+  | tnullptr31 : type
+  | tnullptr32 : type
+  | tnullptr33 : type
+  | tnullptr34 : type
+  | tnullptr35 : type
+  | tnullptr36 : type
+  | tnullptr37 : type
+  | tnullptr38 : type
+  | tnullptr39 : type
+  | Tarch : type -> type -> type
+  | Tbla : bla -> type
+  | Tblu : blu -> type
+  | Tbli : bli -> type
+with bla :=
+| bla1 : type -> bla
+| bla2 : type -> bla
+| bla3 : type -> bla
+| bla4 : type -> bla
+| bla5 : type -> bla
+with blu :=
+| blu1 : type -> blu
+| blu2 : type -> blu
+| blu3 : type -> blu
+| blu4 : type -> blu
+| blu5 : type -> blu
+with bli :=
+| bli1 : type -> bli
+| bli2 : type -> bli
+| bli3 : type -> bli
+| bli4 : type -> bli
+| bli5 : type -> bli
+.
+
+
+#[local] Notation EQ_DEC T := (forall x y : T, {x = y} + {~ x = y}) (only parsing).
+
+Lemma type_eq_dec' : EQ_DEC type
+with bla_eq_dec' : EQ_DEC bla
+with blu_eq_dec' : EQ_DEC blu
+with bli_eq_dec' : EQ_DEC bli.
+Proof.
+  all: intros x y.
+  all: pose (type_eq_dec' : EQ_DEC type).
+  all: pose (bla_eq_dec' : EQ_DEC bla).
+  all: pose (blu_eq_dec' : EQ_DEC blu).
+  all: pose (bli_eq_dec' : EQ_DEC bli).
+  all: decide equality.
+Defined.
+
+Definition type_eq_dec := Eval lazy zeta delta [type_eq_dec'] in type_eq_dec'.
+Definition bla_eq_dec :=  Eval lazy zeta delta [bla_eq_dec']  in bla_eq_dec'.
+Definition blu_eq_dec :=  Eval lazy zeta delta [blu_eq_dec']  in blu_eq_dec'.
+Definition bli_eq_dec :=  Eval lazy zeta delta [bli_eq_dec']  in bli_eq_dec'.
+
+Definition Decision := fun P : Prop => {P} + {~ P}.
+Definition RelDecision := fun {A B : Type} (R : A -> B -> Prop) => forall (x : A) (y : B), Decision (R x y).
+Definition bool_decide {P:Prop} : {P} + {~P} -> bool :=
+    fun x => match x with | left _ => true | right _ => false end.
+Definition decide_rel {A B : Type} (R : A -> B -> Prop) (RelDecision : RelDecision R) : forall (x : A) (y : B), Decision (R x y) :=
+  RelDecision.
+
+Goal (if if bool_decide (decide_rel _ type_eq_dec (Tarch Tvoid Tvoid) (Tarch Tvoid Tvoid)) then true else false then True else False).
+  Succeed Instructions cbn.
+  Timeout 1 time "cbn  " cbn.        (* Tactic call cbn   ran for 0.707 secs (0.706u,0.s) (su *)
+Abort.
+
+(* issue #18619 *)
+Fixpoint test (n : nat) (b : bool) :=
+  match n with
+  | 0 => if b then true else false
+  | S n => test n b
+  end.
+Arguments test : simpl nomatch.
+Goal forall b, test 5000 b = b.
+Proof. intros.
+  Succeed Instructions cbn.
+  Timeout 1 assert_succeeds ((time cbn);   lazymatch goal with |- test 0 b = b => idtac end). (* 3s *)
+Abort.
+
+(* issue #15720 *)
+Module Import PTELE.
+  Inductive tele : Type :=
+  | tO : tele
+  | tS {X : Type} : (X -> tele) -> tele.
+
+  Fixpoint tele_fun (t : tele) (T: Type) : Type :=
+    match t with
+    | tO => T
+    | tS F => forall x, tele_fun (F x) T
+    end.
+  Notation "t -pt> T" := (tele_fun t T)(format "t  -pt>  T", at level 99, T at level 200, right associativity).
+
+  Module FixArgs.
+  Section ArgRecord.
+    #[local] Set Primitive Projections.
+    Context {A : Type} {P : A -> Type}.
+    Record arg := taS' { arg_hd : A; arg_tl : P arg_hd }.
+  End ArgRecord.
+
+  Record argO := taO {}.
+  Arguments arg {_} _.
+
+  (* Eeverything below is identical to code in [FixArgsNonPrim] *)
+  Fixpoint tele_arg (t : tele) : Type :=
+    match t return Type with
+    | tO => argO
+    | tS F => arg (fun x => tele_arg (F x))
+    end.
+  Definition taS {X F} (x : X) (a : tele_arg (F x)) : tele_arg (tS F) :=
+    taS' x a.
+
+  Fixpoint tele_app {t : tele} {T} : tele_fun t T -> tele_arg t -> T :=
+    match t with
+    | tO => fun f _ => f
+    | tS F => fun f '(taS' x args) => tele_app (f x) args
+    end.
+  #[global] Arguments tele_app {!_ _} _ !_ /.
+
+  Fixpoint tele_bind {t:tele} {T} : (tele_arg t -> T) -> t -pt> T :=
+    match t with
+    | tO => fun g => g taO
+    | tS F => fun g x => tele_bind (fun a => g (taS x a))
+    end.
+  #[global] Arguments tele_bind {!_ _} _ /.
+
+  End FixArgs.
+
+  Module FixArgsNonPrim.
+
+  Section ArgRecord.
+    #[local] Unset Primitive Projections.
+    Context {A : Type} {P : A -> Type}.
+    Record arg := taS' { arg_hd : A; arg_tl : P arg_hd }.
+  End ArgRecord.
+
+  Record argO := taO {}.
+  Arguments arg {_} _.
+
+  (* Eeverything below is identical to code in [FixArgs] *)
+  Fixpoint tele_arg (t : tele) : Type :=
+    match t return Type with
+    | tO => argO
+    | tS F => arg (fun x => tele_arg (F x))
+    end.
+  Definition taS {X F} (x : X) (a : tele_arg (F x)) : tele_arg (tS F) :=
+    taS' x a.
+  #[global] Arguments taS _ _ _ & _.
+  Coercion tele_arg : tele >-> Sortclass.
+
+  Fixpoint tele_app {t : tele} {T} : tele_fun t T -> tele_arg t -> T :=
+    match t with
+    | tO => fun f _ => f
+    | tS F => fun f '(taS' x args) => tele_app (f x) args
+    end.
+  #[global] Arguments tele_app {!_ _} _ !_ /.
+
+  (** Currying telescopic functions *)
+  Fixpoint tele_bind {t:tele} {T} : (t -> T) -> t -pt> T :=
+    match t with
+    | tO => fun g => g taO
+    | tS F => fun g x => tele_bind (fun a => g (taS x a))
+    end.
+  #[global] Arguments tele_bind {!_ _} _ /.
+
+  End FixArgsNonPrim.
+
+End PTELE.
+
+Fixpoint build_tele (n : nat) : tele :=
+  match n with
+  | 0 => tO
+  | S n => tS (fun _ : nat => build_tele n)
+  end.
+
+Module Prim.
+  Import PTELE.FixArgs.
+  Fixpoint build_fn (n : nat) : build_tele n -pt> nat :=
+    match n as n return build_tele n -pt> nat with
+    | 0 => 0
+    | S n => fun x => build_fn n
+    end.
+
+  Fixpoint add (m n : nat) (p : build_tele n -pt> nat) : build_tele n -pt> nat :=
+    match m with
+    | 0 => p
+    | S m => tele_bind (fun x => 1 + tele_app (add m n p) x)
+    end.
+
+  Succeed Instructions Eval cbn in @add 8    10 (build_fn 10).
+  Timeout 2 Eval cbn     in @add 8    10 (build_fn 10). (* 2.400s *)
+  (* Time Eval cbn     in @add 10   10 (build_fn 10). (* 11s    *) *)
+  (* [m=20] runs out of memory after a while. *)
+End Prim.
+
+Module NonPrim.
+  Import PTELE.FixArgsNonPrim.
+  Fixpoint build_fn (n : nat) : build_tele n -pt> nat :=
+    match n as n return build_tele n -pt> nat with
+    | 0 => 0
+    | S n => fun x => build_fn n
+    end.
+
+  Fixpoint add (m n : nat) (p : build_tele n -pt> nat) : build_tele n -pt> nat :=
+    match m with
+    | 0 => p
+    | S m => tele_bind (fun x => 1 + tele_app (add m n p) x)
+    end.
+
+  (* Time Eval cbn     in @add 2    10 (build_fn 10). (* 0.001s *) *)
+  (* Time Eval cbn     in @add 4    10 (build_fn 10). (* 0.003s *) *)
+  (* Time Eval cbn     in @add 8    10 (build_fn 10). (* 0.006s *) *)
+  (* Time Eval cbn     in @add 10   10 (build_fn 10). (* 0.008s *) *)
+  (* Time Eval cbn     in @add 20   10 (build_fn 10). (* 0.016s *) *)
+  (* Time Eval cbn     in @add 200  10 (build_fn 10). (* 0.17s  *) *)
+
+  Succeed Instructions Eval cbn in @add 2000 10 (build_fn 10).
+  Timeout 1 Eval cbn     in @add 2000 10 (build_fn 10). (* 3.5s   *)
+End NonPrim.
diff --git a/test-suite/success/cbn3.v b/test-suite/success/cbn3.v
new file mode 100644
index 000000000000..8ec909dc1098
--- /dev/null
+++ b/test-suite/success/cbn3.v
@@ -0,0 +1,104 @@
+(* Regression tests for the closure-based cbn implementation. *)
+
+From Ltac2 Require Import Ltac2.
+Set Default Proof Mode "Classic".
+Set Universe Polymorphism.
+
+Ltac2 check_lhs_evar_arg0_is_zero () :=
+  let g := Control.goal () in
+  match Constr.Unsafe.kind g with
+  | Constr.Unsafe.App _ args =>
+    let lhs := Array.get args 1 in
+    match Constr.Unsafe.kind lhs with
+    | Constr.Unsafe.Evar _ eargs =>
+      if Int.equal (Array.length eargs) 0 then Control.throw Assertion_failure
+      else if Constr.equal (Array.get eargs 0) '0 then ()
+      else Control.throw Assertion_failure
+    | _ => Control.throw Assertion_failure
+    end
+  | _ => Control.throw Assertion_failure
+  end.
+
+Section UnderBinders.
+
+  (* [norm_cbn] must keep the real local environment when it descends below
+     products/lambdas.  In particular, reductions below the binder should see
+     a well-formed context, not dummy [Prop] assumptions. *)
+  Goal forall (A : Type) (x : A), (fun y : A => y) x = x.
+  Proof.
+    cbn.
+    lazymatch goal with |- forall (A : Type) (x : A), x = x => idtac end.
+    reflexivity.
+  Qed.
+
+  (* Same issue for local definitions under binders. *)
+  Goal forall (A : Type) (x : A), (let y := (fun z : A => z) x in y) = x.
+  Proof.
+    cbn.
+    lazymatch goal with |- forall (A : Type) (x : A), x = x => idtac end.
+    reflexivity.
+  Qed.
+
+End UnderBinders.
+
+Section CasesAndFixpoints.
+
+  Inductive dep : nat -> Type :=
+  | dep0 : dep 0
+  | depS : forall n, dep n -> dep (S n).
+
+  (* [norm_cbn] also descends through case predicates and branches.  This used
+     to rely on the full annotated case context. *)
+  Goal forall n (d : dep n),
+      match d in dep n return dep n with
+      | dep0 => dep0
+      | depS n d => depS n d
+      end = d.
+  Proof.
+    cbn.
+    intros [] []; reflexivity.
+  Qed.
+
+  (* Recursive bodies are normalized in a context containing the actual
+     recursive types, not anonymous dummy assumptions. *)
+  Goal forall (A : Type) (x : A),
+      (fix go n :=
+         match n with
+         | 0 => x
+         | S n => go n
+         end) 2 = x.
+  Proof.
+    cbn.
+    reflexivity.
+  Qed.
+
+End CasesAndFixpoints.
+
+Section EvarInstances.
+
+  (* When strong cbn normalizes an evar occurrence, skipped/default evar
+     instance entries must be normalized too.  The open term below creates an
+     evar under a local let; cbn contracts the let and must update the evar
+     instance accordingly. *)
+  Goal True.
+  Proof.
+    let T := open_constr:((let x := (fun y : nat => y) 0 in _ = 0)) in
+    enough T by exact I.
+    cbn.
+    ltac2:(check_lhs_evar_arg0_is_zero ()).
+    exact eq_refl.
+  Qed.
+
+  (* Same check under ordinary binders, to exercise evar instances while the
+     reducer is threading a non-empty local environment. *)
+  Goal True.
+  Proof.
+    let T := open_constr:(((fun (A : Type) (x : A) => (fun y : A => y) _ = x) nat 0)) in
+    enough T by exact I.
+    cbn.
+    ltac2:(check_lhs_evar_arg0_is_zero ()).
+    instantiate (1 := x).
+    exact eq_refl.
+  Qed.
+
+End EvarInstances.
diff --git a/test-suite/success/cbn_hott.v b/test-suite/success/cbn_hott.v
new file mode 100644
index 000000000000..fbc397fb5cef
--- /dev/null
+++ b/test-suite/success/cbn_hott.v
@@ -0,0 +1,1773 @@
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-noinit" "-indices-matter") -*- *)
+(* File reduced by coq-bug-minimizer from original input, then from 451 lines to 58 lines, then from 72 lines to 1063 lines, then from 1070 lines to 273 lines, then from 287 lines to 1386 lines, then from 1393 lines to 535 lines, then from 549 lines to 1150 lines, then from 1157 lines to 601 lines, then from 615 lines to 1562 lines, then from 1569 lines to 686 lines, then from 700 lines to 1504 lines, then from 1511 lines to 725 lines, then from 739 lines to 1253 lines, then from 1260 lines to 803 lines, then from 817 lines to 870 lines, then from 877 lines to 812 lines, then from 826 lines to 1201 lines, then from 1208 lines to 864 lines, then from 878 lines to 1089 lines, then from 1096 lines to 921 lines, then from 935 lines to 2032 lines, then from 2039 lines to 946 lines, then from 960 lines to 1000 lines, then from 1007 lines to 952 lines, then from 966 lines to 1021 lines, then from 1028 lines to 983 lines, then from 997 lines to 1238 lines, then from 1245 lines to 1119 lines, then from 1133 lines to 1532 lines, then from 1538 lines to 1275 lines, then from 1289 lines to 1477 lines, then from 1484 lines to 1319 lines, then from 1333 lines to 1447 lines, then from 1454 lines to 1395 lines, then from 1406 lines to 2147 lines, then from 2154 lines to 1554 lines, then from 1565 lines to 2417 lines, then from 2422 lines to 1574 lines, then from 1585 lines to 2475 lines, then from 2481 lines to 1639 lines, then from 1650 lines to 2389 lines, then from 2395 lines to 1776 lines, then from 1787 lines to 3348 lines, then from 3354 lines to 1827 lines, then from 1838 lines to 2550 lines, then from 2554 lines to 1919 lines, then from 1930 lines to 2744 lines, then from 2750 lines to 2076 lines, then from 2087 lines to 2402 lines, then from 2406 lines to 2114 lines, then from 2124 lines to 2222 lines, then from 2228 lines to 2136 lines, then from 2142 lines to 2137 lines, then from 2143 lines to 1766 lines, then from 1772 lines to 1766 lines, then from 0 lines to 1766 lines *)
+(* coqc version 9.3+alpha compiled with OCaml 5.4.0
+   coqtop version 9.3+alpha
+   Expected coqc runtime on this file: 0.000 sec
+   Expected coqc peak memory usage on this file: 0.0 kb *)
+
+Require Corelib.Init.Ltac.
+
+Inductive False : Prop := .
+Axiom proof_admitted : False.
+Tactic Notation "admit" := abstract case proof_admitted.
+
+Declare ML Module "rocq-runtime.plugins.ltac".
+
+Global Set Default Proof Mode "Classic".
+
+Global Set Universe Polymorphism.
+
+Global Unset Strict Universe Declaration.
+
+Global Set Primitive Projections.
+Create HintDb typeclass_instances discriminated.
+Reserved Notation "x -> y" (at level 99, right associativity, y at level 200).
+Reserved Notation "~ x" (at level 35, right associativity).
+
+Reserved Notation "x = y  :>  T"
+(at level 70, y at next level, no associativity).
+
+Reserved Notation "x + y" (at level 50, left associativity).
+Reserved Notation "x * y" (at level 40, left associativity).
+
+Reserved Notation "{ x : A  & P }" (at level 0, x at level 99).
+Reserved Notation "p @ q" (at level 20).
+Reserved Notation "p # x" (right associativity, at level 65).
+Reserved Notation "p @@ q" (at level 20).
+Reserved Notation "f == g" (at level 70, no associativity).
+
+Reserved Notation "A <~> B" (at level 85).
+
+Reserved Infix "$->" (at level 99).
+Reserved Infix "$<~>" (at level 85).
+Reserved Infix "$o" (at level 40, left associativity).
+Reserved Infix "$==" (at level 70).
+Reserved Infix "$@" (at level 30).
+Reserved Infix "$@L" (at level 30).
+Reserved Infix "$@R" (at level 30).
+Reserved Infix "$=>" (at level 99).
+Reserved Notation "g 'o' f" (at level 40, left associativity).
+
+Declare Scope core_scope.
+Declare Scope fibration_scope.
+Delimit Scope function_scope with function.
+Delimit Scope type_scope with type.
+Delimit Scope path_scope with path.
+Global Open Scope path_scope.
+Global Open Scope fibration_scope.
+Global Open Scope function_scope.
+Global Open Scope type_scope.
+Global Open Scope core_scope.
+Module Export Overture.
+
+Local Unset Elimination Schemes.
+
+Notation "A -> B" := (forall (_ : A), B) : type_scope.
+
+Inductive sum (A B : Type) : Type :=
+| inl : A -> sum A B
+| inr : B -> sum A B.
+Scheme sum_ind := Induction for sum Sort Type.
+Arguments sum_ind {A B} P f g : rename.
+
+Notation "x + y" := (sum x y) : type_scope.
+
+Arguments inl {A B} _ , [A] B _.
+Arguments inr {A B} _ , A [B] _.
+
+Record prod (A B : Type) := pair { fst : A ; snd : B }.
+
+Arguments pair {A B} _ _.
+Arguments fst {A B} _ / .
+Arguments snd {A B} _ / .
+
+Notation "x * y" := (prod x y) : type_scope.
+Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope.
+
+#[export] Hint Resolve pair inl inr : core.
+
+Local Set Typeclasses Strict Resolution.
+
+Definition Relation (A : Type) := A -> A -> Type.
+
+Class Reflexive {A} (R : Relation A) :=
+  reflexivity : forall x : A, R x x.
+
+Class Transitive {A} (R : Relation A) :=
+  transitivity : forall x y z, R x y -> R y z -> R x z.
+
+Ltac old_reflexivity := reflexivity.
+Tactic Notation "reflexivity" :=
+  old_reflexivity
+|| (intros;
+  let R := match goal with |- ?R ?x ?y => constr:(R) end in
+  let pre_proof_term_head := constr:(@reflexivity _ R _) in
+  let proof_term_head := (eval cbn in pre_proof_term_head) in
+  apply (proof_term_head : forall x, R x x)).
+
+Tactic Notation "etransitivity" open_constr(y) :=
+  let R := match goal with |- ?R ?x ?z => constr:(R) end in
+  let x := match goal with |- ?R ?x ?z => constr:(x) end in
+  let z := match goal with |- ?R ?x ?z => constr:(z) end in
+  let pre_proof_term_head := constr:(@transitivity _ R _) in
+  let proof_term_head := (eval cbn in pre_proof_term_head) in
+  refine (proof_term_head x y z _ _); [ change (R x y) | change (R y z) ].
+
+Tactic Notation "etransitivity" := etransitivity _.
+
+Notation Type0 := Set.
+
+Record sig {A} (P : A -> Type) := exist {
+  proj1 : A ;
+  proj2 : P proj1 ;
+}.
+
+Arguments exist {A}%_type P%_type _ _.
+Notation "{ x : A  & P }" := (sig (fun x:A => P)) : type_scope.
+
+Notation "( x ; y )" := (exist _ x y) : fibration_scope.
+
+Notation idmap := (fun x => x).
+
+Notation compose := (fun g f x => g (f x)).
+
+Notation "g 'o' f" := (compose g%function f%function) : function_scope.
+
+Inductive paths {A : Type} (a : A) : A -> Type :=
+  idpath : paths a a.
+
+Arguments idpath {A a} , [A] a.
+
+Scheme paths_ind := Induction for paths Sort Type.
+
+Notation "x = y :> A" := (@paths A x y) : type_scope.
+Notation "x = y" := (x = y :>_) : type_scope.
+Definition inverse {A : Type} {x y : A} (p : x = y) : y = x.
+exact (match p with idpath => idpath end).
+Defined.
+
+Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z :=
+  match p, q with idpath, idpath => idpath end.
+
+Notation "1" := idpath : path_scope.
+
+Notation "p @ q" := (concat p%path q%path) : path_scope.
+
+Notation "p ^" := (inverse p%path) : path_scope.
+Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y.
+Admitted.
+
+Notation "p # u" := (transport _ p u) (only parsing) : path_scope.
+Definition ap {A B : Type} (f : A -> B) {x y : A} (p : x = y) : f x = f y.
+exact (match p with idpath => idpath end).
+Defined.
+Definition apD {A:Type} {B:A->Type} (f:forall a:A, B a) {x y:A} (p:x=y):
+  p # (f x) = f y.
+Admitted.
+
+Definition pointwise_paths A (P : A -> Type) (f g : forall x, P x)
+  := forall x, f x = g x.
+
+Instance transitive_pointwise_paths A P
+  : Transitive (pointwise_paths A P).
+Admitted.
+
+Global Arguments pointwise_paths {A}%_type_scope {P} (f g)%_function_scope.
+
+Notation "f == g" := (pointwise_paths f g) : type_scope.
+
+Class IsEquiv {A B : Type} (f : A -> B) := {
+  equiv_inv : B -> A ;
+  eisretr : f o equiv_inv == idmap ;
+  eissect : equiv_inv o f == idmap ;
+  eisadj : forall x : A, eisretr (f x) = ap f (eissect x) ;
+}.
+
+Arguments eisretr {A B}%_type_scope f%_function_scope {_} _.
+Arguments eissect {A B}%_type_scope f%_function_scope {_} _.
+
+Record Equiv A B := {
+  equiv_fun : A -> B ;
+  equiv_isequiv :: IsEquiv equiv_fun
+}.
+
+Coercion equiv_fun : Equiv >-> Funclass.
+
+Notation "A <~> B" := (Equiv A B) : type_scope.
+
+Notation "f ^-1" := (@equiv_inv _ _ f _) : function_scope.
+
+Inductive Empty : Type0 := .
+
+Definition not (A : Type) := A -> Empty.
+Notation "~ x" := (not x) : type_scope.
+
+End Overture.
+
+Tactic Notation "do_with_holes" tactic3(x) uconstr(p) :=
+  x uconstr:(p) ||
+  x uconstr:(p _) ||
+  x uconstr:(p _ _) ||
+  x uconstr:(p _ _ _) ||
+  x uconstr:(p _ _ _ _) ||
+  x uconstr:(p _ _ _ _ _) ||
+  x uconstr:(p _ _ _ _ _ _) ||
+  x uconstr:(p _ _ _ _ _ _ _) ||
+  x uconstr:(p _ _ _ _ _ _ _ _) ||
+  x uconstr:(p _ _ _ _ _ _ _ _ _) ||
+  x uconstr:(p _ _ _ _ _ _ _ _ _ _) ||
+  x uconstr:(p _ _ _ _ _ _ _ _ _ _ _) ||
+  x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _) ||
+  x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _) ||
+  x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
+  x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
+  x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
+  x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
+  x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
+  x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
+  x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
+  x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
+  x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
+  x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
+  x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
+  x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
+  x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
+  x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
+  x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
+  x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
+  x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _).
+Class IsGlobalAxiom (A : Type) : Type0 := {}.
+
+Ltac is_global_axiom A := let _ := constr:(_ : IsGlobalAxiom A) in idtac.
+
+Ltac global_axiom := try match goal with
+    | |- ?G  => is_global_axiom G; exact _
+end.
+
+Tactic Notation "srefine" uconstr(term) := simple refine term.
+
+Tactic Notation "nrefine" uconstr(term) := notypeclasses refine term; global_axiom.
+
+Tactic Notation "snrefine" uconstr(term) := simple notypeclasses refine term; global_axiom.
+
+Tactic Notation "napply" uconstr(term)
+  := do_with_holes ltac:(fun x => nrefine x) term.
+
+Tactic Notation "rapply" uconstr(term)
+  := do_with_holes ltac:(fun x => assert_succeeds (nrefine x); refine x) term.
+
+Tactic Notation "tapply" uconstr(term)
+  := do_with_holes ltac:(fun x => refine x) term.
+
+Tactic Notation "snapply" uconstr(term)
+  := do_with_holes ltac:(fun x => snrefine x) term.
+
+Tactic Notation "srapply" uconstr(term)
+  := do_with_holes ltac:(fun x => assert_succeeds (simple notypeclasses refine x); srefine x) term.
+
+Tactic Notation "lhs" tactic3(tac) := nrefine (ltac:(tac) @ _).
+
+Ltac done :=
+  trivial; intros; solve
+    [ repeat first
+      [ solve [trivial]
+      | solve [symmetry; trivial]
+      | reflexivity
+
+      | contradiction
+      | split ]
+    | match goal with
+      H : ~ _ |- _ => solve [destruct H; trivial]
+      end ].
+
+Tactic Notation "by" tactic(tac) :=
+  tac; done.
+Definition concat_p_pp {A : Type} {x y z t : A} (p : x = y) (q : y = z) (r : z = t) :
+  p @ (q @ r) = (p @ q) @ r.
+Admitted.
+Definition concat_pp_p {A : Type} {x y z t : A} (p : x = y) (q : y = z) (r : z = t) :
+  (p @ q) @ r = p @ (q @ r).
+Admitted.
+Definition concat_V_pp {A : Type} {x y z : A} (p : x = y) (q : y = z) :
+  p^ @ (p @ q) = q.
+Admitted.
+
+Definition moveR_pV {A : Type} {x y z : A} (p : z = x) (q : y = z) (r : y = x) :
+  r = q @ p -> r @ p^ = q.
+Admitted.
+Definition ap_V {A B : Type} (f : A -> B) {x y : A} (p : x = y) :
+  ap f (p^) = (ap f p)^.
+Admitted.
+
+Definition transport_const {A B : Type} {x1 x2 : A} (p : x1 = x2) (y : B)
+  : transport (fun x => B) p y = y.
+Admitted.
+
+Lemma apD_const {A B} {x y : A} (f : A -> B) (p: x = y) :
+  apD f p = transport_const p (f x) @ ap f p.
+Admitted.
+Definition concat2 {A} {x y z : A} {p p' : x = y} {q q' : y = z} (h : p = p') (h' : q = q')
+  : p @ q = p' @ q'.
+Admitted.
+
+Notation "p @@ q" := (concat2 p q)%path : path_scope.
+Definition whiskerL {A : Type} {x y z : A} (p : x = y)
+  {q r : y = z} (h : q = r) : p @ q = p @ r.
+Admitted.
+Definition whiskerR {A : Type} {x y z : A} {p q : x = y}
+  (h : p = q) (r : y = z) : p @ r = q @ r.
+Admitted.
+Definition cancelL {A} {x y z : A} (p : x = y) (q r : y = z)
+: (p @ q = p @ r) -> (q = r).
+exact (fun h => (concat_V_pp p q)^ @ whiskerL p^ h @ (concat_V_pp p r)).
+Defined.
+
+Class IsGraph (A : Type) :=
+{
+  Hom : A -> A -> Type
+}.
+
+Notation "a $-> b" := (Hom a b).
+
+Class Is01Cat (A : Type) `{IsGraph A} :=
+{
+  Id  : forall (a : A), a $-> a;
+  cat_comp : forall (a b c : A), (b $-> c) -> (a $-> b) -> (a $-> c);
+}.
+Arguments cat_comp {A _ _ a b c} _ _.
+Notation "g $o f" := (cat_comp g f).
+Definition cat_postcomp {A} `{Is01Cat A} (a : A) {b c : A} (g : b $-> c)
+  : (a $-> b) -> (a $-> c).
+exact (cat_comp g).
+Defined.
+Definition cat_precomp {A} `{Is01Cat A} {a b : A} (c : A) (f : a $-> b)
+  : (b $-> c) -> (a $-> c).
+Admitted.
+
+Class Is0Gpd (A : Type) `{Is01Cat A} :=
+  { gpd_rev : forall {a b : A}, (a $-> b) -> (b $-> a) }.
+
+Definition GpdHom {A} `{Is0Gpd A} (a b : A) := a $-> b.
+Notation "a $== b" := (GpdHom a b).
+Instance reflexive_GpdHom {A} `{Is0Gpd A}
+  : Reflexive GpdHom.
+Admitted.
+Definition gpd_comp {A} `{Is0Gpd A} {a b c : A}
+  : (a $== b) -> (b $== c) -> (a $== c).
+Admitted.
+Infix "$@" := gpd_comp.
+
+Notation "p ^$" := (gpd_rev p).
+
+Class Is0Functor {A B : Type} `{IsGraph A} `{IsGraph B} (F : A -> B)
+  := { fmap : forall (a b : A) (f : a $-> b), F a $-> F b }.
+
+Arguments Build_Is0Functor {A B isgraph_A isgraph_B} F fmap : rename.
+Arguments fmap {A B isgraph_A isgraph_B} F {is0functor_F a b} f : rename.
+
+Class Is2Graph (A : Type) `{IsGraph A}
+  := isgraph_hom : forall (a b : A), IsGraph (a $-> b).
+Existing Instance isgraph_hom | 20.
+
+Class Is1Cat (A : Type) `{!IsGraph A, !Is2Graph A, !Is01Cat A} :=
+{
+  is01cat_hom :: forall (a b : A), Is01Cat (a $-> b) ;
+  is0gpd_hom :: forall (a b : A), Is0Gpd (a $-> b) ;
+  is0functor_postcomp :: forall (a b c : A) (g : b $-> c), Is0Functor (cat_postcomp a g) ;
+  is0functor_precomp :: forall (a b c : A) (f : a $-> b), Is0Functor (cat_precomp c f) ;
+  cat_assoc : forall (a b c d : A) (f : a $-> b) (g : b $-> c) (h : c $-> d),
+    (h $o g) $o f $== h $o (g $o f);
+  cat_assoc_opp : forall (a b c d : A) (f : a $-> b) (g : b $-> c) (h : c $-> d),
+    h $o (g $o f) $== (h $o g) $o f;
+  cat_idl : forall (a b : A) (f : a $-> b), Id b $o f $== f;
+  cat_idr : forall (a b : A) (f : a $-> b), f $o Id a $== f;
+}.
+
+Arguments cat_assoc {_ _ _ _ _ _ _ _ _} f g h.
+Arguments cat_idl {_ _ _ _ _ _ _} f.
+Arguments cat_idr {_ _ _ _ _ _ _} f.
+Definition cat_postwhisker {A} `{Is1Cat A} {a b c : A}
+           {f g : a $-> b} (h : b $-> c) (p : f $== g)
+  : h $o f $== h $o g.
+Admitted.
+Notation "h $@L p" := (cat_postwhisker h p).
+Definition cat_prewhisker {A} `{Is1Cat A} {a b c : A}
+           {f g : b $-> c} (p : f $== g) (h : a $-> b)
+  : f $o h $== g $o h.
+Admitted.
+Notation "p $@R h" := (cat_prewhisker p h).
+
+Class Is1Cat_Strong (A : Type)`{!IsGraph A, !Is2Graph A, !Is01Cat A} :=
+{
+  is01cat_hom_strong : forall (a b : A), Is01Cat (a $-> b) ;
+  is0gpd_hom_strong : forall (a b : A), Is0Gpd (a $-> b) ;
+  is0functor_postcomp_strong : forall (a b c : A) (g : b $-> c),
+    Is0Functor (cat_postcomp a g) ;
+  is0functor_precomp_strong : forall (a b c : A) (f : a $-> b),
+    Is0Functor (cat_precomp c f) ;
+  cat_assoc_strong : forall (a b c d : A)
+    (f : a $-> b) (g : b $-> c) (h : c $-> d),
+    (h $o g) $o f = h $o (g $o f) ;
+  cat_assoc_opp_strong : forall (a b c d : A)
+    (f : a $-> b) (g : b $-> c) (h : c $-> d),
+    h $o (g $o f) = (h $o g) $o f ;
+  cat_idl_strong : forall (a b : A) (f : a $-> b), Id b $o f = f ;
+  cat_idr_strong : forall (a b : A) (f : a $-> b), f $o Id a = f ;
+}.
+
+Definition is1cat_is1cat_strong (A : Type) `{Is1Cat_Strong A}
+  : Is1Cat A.
+Admitted.
+
+Hint Immediate is1cat_is1cat_strong : typeclass_instances.
+
+Class Is1Functor {A B : Type} `{Is1Cat A} `{Is1Cat B}
+  (F : A -> B) `{!Is0Functor F} :=
+{
+  fmap2 : forall a b (f g : a $-> b), (f $== g) -> (fmap F f $== fmap F g) ;
+  fmap_id : forall a, fmap F (Id a) $== Id (F a);
+  fmap_comp : forall a b c (f : a $-> b) (g : b $-> c),
+    fmap F (g $o f) $== fmap F g $o fmap F f;
+}.
+
+Arguments fmap2 {A B
+  isgraph_A is2graph_A is01cat_A is1cat_A
+  isgraph_B is2graph_B is01cat_B is1cat_B}
+  F {is0functor_F is1functor_F a b f g} p : rename.
+
+  #[export] Instance is0functor_idmap {A : Type} `{IsGraph A} : Is0Functor idmap.
+Admitted.
+
+Instance is0functor_compose {A B C : Type}
+  `{IsGraph A, IsGraph B, IsGraph C}
+  (F : A -> B) `{!Is0Functor F} (G : B -> C) `{!Is0Functor G}
+  : Is0Functor (G o F).
+Admitted.
+
+Instance isequiv_idmap (A : Type) : IsEquiv idmap | 0 :=
+  Build_IsEquiv A A idmap idmap (fun _ => 1) (fun _ => 1) (fun _ => 1).
+Definition equiv_idmap (A : Type) : A <~> A.
+exact (Build_Equiv A A idmap _).
+Defined.
+
+Arguments equiv_idmap {A} , A.
+
+Section Adjointify.
+
+  Context {A B : Type} (f : A -> B) (g : B -> A).
+  Context (isretr : f o g == idmap) (issect : g o f == idmap).
+
+  Let issect' := fun x =>
+    ap g (ap f (issect x)^)  @  ap g (isretr (f x))  @  issect x.
+
+  Local Definition is_adjoint' (a : A) : isretr (f a) = ap f (issect' a).
+Admitted.
+Definition isequiv_adjointify : IsEquiv f.
+exact (Build_IsEquiv A B f g isretr issect' is_adjoint').
+Defined.
+Definition equiv_adjointify : A <~> B.
+exact (Build_Equiv A B f isequiv_adjointify).
+Defined.
+
+End Adjointify.
+
+Definition equiv_homotopic_inverse {A B} (e : A <~> B)
+  {f : A -> B} {g : B -> A} (h : f == e) (k : g == e^-1)
+  : A <~> B.
+Proof.
+  snapply equiv_adjointify.
+  -
+ exact f.
+  -
+ exact g.
+  -
+ intro a.
+ exact (ap f (k a) @ h _ @ eisretr e a).
+  -
+ intro b.
+ exact (ap g (h b) @ k _ @ eissect e b).
+Defined.
+
+Definition transport_paths_Fr {A B : Type} {g : A -> B} {y1 y2 : A} {x : B}
+  (p : y1 = y2) (q : x = g y1)
+  : transport (fun y => x = g y) p q = q @ (ap g p).
+Admitted.
+Definition equiv_p1_1q {A : Type} {x y : A} {p q : x = y}
+  : p = q <~> p @ 1 = 1 @ q.
+Admitted.
+
+Class HasEquivs (A : Type) `{Is1Cat A} :=
+{
+  CatEquiv' : A -> A -> Type where "a $<~> b" := (CatEquiv' a b);
+  CatIsEquiv' : forall a b, (a $-> b) -> Type;
+  cate_fun' : forall a b, (a $<~> b) -> (a $-> b);
+  cate_isequiv' : forall a b (f : a $<~> b), CatIsEquiv' a b (cate_fun' a b f);
+  cate_buildequiv' : forall a b (f : a $-> b), CatIsEquiv' a b f -> CatEquiv' a b;
+  cate_buildequiv_fun' : forall a b (f : a $-> b) (fe : CatIsEquiv' a b f),
+      cate_fun' a b (cate_buildequiv' a b f fe) $== f;
+  cate_inv' : forall a b (f : a $<~> b), b $-> a;
+  cate_issect' : forall a b (f : a $<~> b),
+    cate_inv' _ _ f $o cate_fun' _ _ f $== Id a;
+  cate_isretr' : forall a b (f : a $<~> b),
+      cate_fun' _ _ f $o cate_inv' _ _ f $== Id b;
+  catie_adjointify' : forall a b (f : a $-> b) (g : b $-> a)
+    (r : f $o g $== Id b) (s : g $o f $== Id a), CatIsEquiv' a b f;
+}.
+
+Definition CatEquiv {A} `{HasEquivs A} (a b : A)
+  := @CatEquiv' A _ _ _ _ _ a b.
+
+Notation "a $<~> b" := (CatEquiv a b).
+Definition cate_fun {A} `{HasEquivs A} {a b : A} (f : a $<~> b)
+  : a $-> b.
+exact (@cate_fun' A _ _ _ _ _ a b f).
+Defined.
+
+Coercion cate_fun : CatEquiv >-> Hom.
+
+Class CatIsEquiv {A} `{HasEquivs A} {a b : A} (f : a $-> b)
+  := catisequiv : CatIsEquiv' a b f.
+Instance cate_isequiv {A} `{HasEquivs A} {a b : A} (f : a $<~> b)
+  : CatIsEquiv f.
+Admitted.
+Definition Build_CatEquiv {A} `{HasEquivs A} {a b : A}
+           (f : a $-> b) {fe : CatIsEquiv f}
+  : a $<~> b.
+exact (cate_buildequiv' a b f fe).
+Defined.
+Definition cate_buildequiv_fun {A} `{HasEquivs A} {a b : A}
+           (f : a $-> b) {fe : CatIsEquiv f}
+  : cate_fun (Build_CatEquiv f) $== f.
+Admitted.
+Definition catie_adjointify {A} `{HasEquivs A} {a b : A}
+           (f : a $-> b) (g : b $-> a)
+           (r : f $o g $== Id b) (s : g $o f $== Id a)
+  : CatIsEquiv f.
+exact (catie_adjointify' a b f g r s).
+Defined.
+Definition cate_adjointify {A} `{HasEquivs A} {a b : A}
+           (f : a $-> b) (g : b $-> a)
+           (r : f $o g $== Id b) (s : g $o f $== Id a)
+  : a $<~> b.
+exact (Build_CatEquiv f (fe:=catie_adjointify f g r s)).
+Defined.
+
+Definition cate_inv {A} `{HasEquivs A} {a b : A} (f : a $<~> b) : b $<~> a.
+Proof.
+  simple refine (cate_adjointify _ _ _ _).
+  -
+ exact (cate_inv' a b f).
+  -
+ exact f.
+  -
+ exact (cate_issect' a b f).
+  -
+ exact (cate_isretr' a b f).
+Defined.
+
+Notation "f ^-1$" := (cate_inv f).
+
+Definition cate_issect {A} `{HasEquivs A} {a b : A} (f : a $<~> b)
+  : f^-1$ $o f $== Id a.
+Admitted.
+Definition cate_isretr {A} `{HasEquivs A} {a b : A} (f : a $<~> b)
+  : f $o f^-1$ $== Id b.
+Admitted.
+
+Definition compose_catie_isretr {A} `{HasEquivs A} {a b c : A}
+  (g : b $<~> c) (f : a $<~> b)
+  : g $o f $o (f^-1$ $o g^-1$) $== Id c.
+Admitted.
+Definition compose_catie_issect {A} `{HasEquivs A} {a b c : A}
+  (g : b $<~> c) (f : a $<~> b)
+  : (f^-1$ $o g^-1$ $o (g $o f) $== Id a).
+Admitted.
+
+Instance compose_catie {A} `{HasEquivs A} {a b c : A}
+  (g : b $<~> c) (f : a $<~> b)
+  : CatIsEquiv (g $o f).
+Proof.
+  refine (catie_adjointify _ (f^-1$ $o g^-1$) _ _).
+  -
+ apply compose_catie_isretr.
+  -
+ apply compose_catie_issect.
+Defined.
+
+Class Cat_IsBiInv {A} `{Is1Cat A} {x y : A} (f : x $-> y) := {
+  cat_equiv_inv : y $-> x;
+  cat_eisretr : f $o cat_equiv_inv $== Id y;
+  cat_equiv_inv' : y $-> x;
+  cat_eissect' : cat_equiv_inv' $o f $== Id x;
+}.
+
+Arguments cat_equiv_inv {A}%_type_scope { _ _ _ _ x y} f {_}.
+Arguments cat_eisretr {A}%_type_scope { _ _ _ _ x y} f {_}.
+
+Arguments Build_Cat_IsBiInv {A}%_type_scope {_ _ _ _ x y f} cat_equiv_inv cat_eisretr cat_equiv_inv' cat_eissect'.
+
+Record Cat_BiInv A `{Is1Cat A} (x y : A) := {
+  cat_equiv_fun :> x $-> y;
+  cat_equiv_isequiv : Cat_IsBiInv cat_equiv_fun;
+}.
+
+Existing Instance cat_equiv_isequiv.
+Definition cat_eissect {A} `{Is1Cat A} {x y : A} (f : x $-> y) {bif : Cat_IsBiInv f}
+  : cat_equiv_inv f $o f $== Id x.
+Admitted.
+
+Definition cat_hasequivs A `{Is1Cat A} : HasEquivs A.
+Proof.
+  srapply Build_HasEquivs; intros x y.
+  1: exact (Cat_BiInv _ x y).
+  all:intros f; cbn beta in *.
+  -
+ exact (Cat_IsBiInv f).
+  -
+ exact f.
+  -
+ exact _.
+  -
+ apply Build_Cat_BiInv.
+  -
+ intros; reflexivity.
+  -
+ exact (cat_equiv_inv f).
+  -
+ apply cat_eissect.
+  -
+ apply cat_eisretr.
+  -
+ intros g r s.
+    exact (Build_Cat_IsBiInv g r g s).
+Defined.
+
+Ltac intros_of_type A :=
+  repeat match goal with |- forall (a : A), _ => intro a end.
+
+Section Induced_category.
+  Context {A B : Type} (f : A -> B).
+
+  Local Instance isgraph_induced `{IsGraph B} : IsGraph A.
+  Proof.
+    napply Build_IsGraph.
+    intros a1 a2.
+    exact (f a1 $-> f a2).
+  Defined.
+
+  Local Instance is01cat_induced `{Is01Cat B} : Is01Cat A.
+  Proof.
+    napply Build_Is01Cat; intros_of_type A; cbn.
+    +
+ apply Id.
+    +
+ exact cat_comp.
+  Defined.
+
+  Local Instance is2graph_induced `{Is2Graph B} : Is2Graph A.
+  Proof.
+    constructor; cbn.
+apply isgraph_hom.
+  Defined.
+
+  Local Instance is1cat_induced `{Is1Cat B} : Is1Cat A.
+Admitted.
+
+  Definition hasequivs_induced `{HasEquivs B} : HasEquivs A.
+  Proof.
+    srapply Build_HasEquivs; intros a b; cbn.
+    +
+ exact (f a $<~> f b).
+    +
+ apply CatIsEquiv'.
+    +
+ exact cate_fun.
+    +
+ apply cate_isequiv'.
+    +
+ apply cate_buildequiv'.
+    +
+ napply cate_buildequiv_fun'.
+    +
+ apply cate_inv'.
+    +
+ napply cate_issect'.
+    +
+ napply cate_isretr'.
+    +
+ napply catie_adjointify'.
+  Defined.
+
+End Induced_category.
+Definition Square@{u v w} {A : Type@{u}} `{Is1Cat@{u w v} A} {x00 x20 x02 x22 : A}
+  (f01 : x00 $-> x02) (f21 : x20 $-> x22) (f10 : x00 $-> x20) (f12 : x02 $-> x22)
+  : Type@{w}.
+exact (f21 $o f10 $== f12 $o f01).
+Defined.
+
+Section Squares.
+
+  Context {A : Type} `{Is1Cat A} {x x' x00 x20 x40 x02 x22 x42 x04 x24 x44 : A}
+    {f10 f10' : x00 $-> x20} {f30 : x20 $-> x40}
+    {f12 f12' : x02 $-> x22} {f32 : x22 $-> x42}
+    {f14 : x04 $-> x24} {f34 : x24 $-> x44}
+    {f01 f01' : x00 $-> x02} {f21 f21' : x20 $-> x22} {f41 f41' : x40 $-> x42}
+    {f03 : x02 $-> x04} {f23 : x22 $-> x24} {f43 : x42 $-> x44}.
+Definition transpose (s : Square f01 f21 f10 f12) : Square f10 f12 f01 f21.
+admit.
+Defined.
+
+  Definition hinverse {HE : HasEquivs A} (f10 : x00 $<~> x20) (f12 : x02 $<~> x22) (s : Square f01 f21 f10 f12)
+    : Square f21 f01 f10^-1$ f12^-1$
+    := (cat_idl _)^$ $@ ((cate_issect f12)^$ $@R _) $@ cat_assoc _ _ _
+      $@ (_ $@L ((cat_assoc _ _ _)^$ $@ (s^$ $@R _) $@ cat_assoc _ _ _
+      $@ (_ $@L cate_isretr f10) $@ cat_idr _)).
+
+End Squares.
+
+Section Squares2.
+
+  Context {A : Type} `{HasEquivs A}
+    {x x' x00 x20 x40 x02 x22 x42 x04 x24 x44 : A}
+    {f10 f10' : x00 $-> x20} {f30 : x20 $-> x40}
+    {f12 f12' : x02 $-> x22} {f32 : x22 $-> x42}
+    {f14 : x04 $-> x24} {f34 : x24 $-> x44}
+    {f01 f01' : x00 $-> x02} {f21 f21' : x20 $-> x22} {f41 f41' : x40 $-> x42}
+    {f03 : x02 $-> x04} {f23 : x22 $-> x24} {f43 : x42 $-> x44}.
+
+  Definition vinverse (f01 : x00 $<~> x02) (f21 : x20 $<~> x22) (s : Square f01 f21 f10 f12)
+    : Square (f01^-1$) (f21^-1$) f12 f10
+    := transpose (hinverse _ _ (transpose s)).
+
+End Squares2.
+
+Definition Transformation {A : Type} {B : A -> Type} `{forall x, IsGraph (B x)}
+  (F G : forall (x : A), B x)
+  := forall (a : A), F a $-> G a.
+
+Identity Coercion fun_trans : Transformation >-> Funclass.
+
+Notation "F $=> G" := (Transformation F G).
+Definition trans_id {A B : Type} `{Is01Cat B} (F : A -> B)
+  : F $=> F.
+exact (fun a => Id (F a)).
+Defined.
+Definition trans_comp {A B : Type} `{Is01Cat B}
+           {F G K : A -> B} (gamma : G $=> K) (alpha : F $=> G)
+  : F $=> K.
+exact (fun a => gamma a $o alpha a).
+Defined.
+
+Class Is1Natural {A B : Type} `{IsGraph A, Is1Cat B}
+  (F : A -> B) `{!Is0Functor F} (G : A -> B) `{!Is0Functor G}
+  (alpha : F $=> G) := Build_Is1Natural' {
+  isnat {a a'} (f : a $-> a') : alpha a' $o fmap F f $== fmap G f $o alpha a;
+
+  isnat_tr {a a'} (f : a $-> a') : fmap G f $o alpha a $== alpha a' $o fmap F f;
+}.
+Arguments isnat {_ _ _ _ _ _ _ _ _ _ _} alpha {alnat _ _} f : rename.
+Arguments isnat_tr {_ _ _ _ _ _ _ _ _ _ _} alpha {alnat _ _} f : rename.
+
+Definition Build_Is1Natural {A B : Type} `{IsGraph A} `{Is1Cat B}
+  {F G : A -> B} `{!Is0Functor F, !Is0Functor G} (alpha : F $=> G)
+  (isnat : forall a a' (f : a $-> a'), alpha a' $o fmap F f $== fmap G f $o alpha a)
+  : Is1Natural F G alpha.
+Admitted.
+
+Instance is1natural_id {A B : Type} `{IsGraph A} `{Is1Cat B}
+  (F : A -> B) `{!Is0Functor F}
+  : Is1Natural F F (trans_id F).
+Admitted.
+
+Instance is1natural_comp {A B : Type} `{IsGraph A} `{Is1Cat B}
+  {F G K : A -> B} `{!Is0Functor F} `{!Is0Functor G} `{!Is0Functor K}
+  (gamma : G $=> K) `{!Is1Natural G K gamma}
+  (alpha : F $=> G) `{!Is1Natural F G alpha}
+  : Is1Natural F K (trans_comp gamma alpha).
+Admitted.
+
+Record NatTrans {A B : Type} `{IsGraph A} `{Is1Cat B} {F G : A -> B}
+  {ff : Is0Functor F} {fg : Is0Functor G} := {
+  #[reversible=no]
+  trans_nattrans :> F $=> G;
+  is1natural_nattrans :: Is1Natural F G trans_nattrans;
+}.
+
+Arguments NatTrans {A B} {isgraph_A}
+  {isgraph_B} {is2graph_B} {is01cat_B} {is1cat_B}
+  F G {is0functor_F} {is0functor_G} : rename.
+Arguments Build_NatTrans {A B isgraph_A isgraph_B is2graph_B is01cat_B is1cat_B
+  F G is0functor_F is0functor_G} alpha isnat_alpha : rename.
+Definition nattrans_id {A B : Type} (F : A -> B)
+  `{IsGraph A, Is1Cat B, !Is0Functor F}
+  : NatTrans F F.
+exact (Build_NatTrans (trans_id F) _).
+Defined.
+Definition nattrans_comp {A B : Type} {F G K : A -> B}
+  `{IsGraph A, Is1Cat B, !Is0Functor F, !Is0Functor G, !Is0Functor K}
+  : NatTrans G K -> NatTrans F G -> NatTrans F K.
+exact (fun alpha beta => Build_NatTrans (trans_comp alpha beta) _).
+Defined.
+
+Record NatEquiv {A B : Type} `{IsGraph A} `{HasEquivs B}
+  {F G : A -> B} `{!Is0Functor F, !Is0Functor G} := {
+  #[reversible=no]
+  cat_equiv_natequiv :> forall a, F a $<~> G a ;
+  is1natural_natequiv :: Is1Natural F G (fun a => cat_equiv_natequiv a) ;
+}.
+
+Arguments NatEquiv {A B} {isgraph_A}
+  {isgraph_B} {is2graph_B} {is01cat_B} {is1cat_B} {hasequivs_B}
+  F G {is0functor_F} {is0functor_G} : rename.
+
+Lemma nattrans_natequiv {A B : Type} `{IsGraph A} `{HasEquivs B}
+  {F G : A -> B} `{!Is0Functor F, !Is0Functor G}
+  : NatEquiv F G -> NatTrans F G.
+Proof.
+  intros alpha.
+  napply Build_NatTrans.
+  exact (is1natural_natequiv alpha).
+Defined.
+Coercion nattrans_natequiv : NatEquiv >-> NatTrans.
+
+Definition Build_NatEquiv' {A B : Type} `{IsGraph A} `{HasEquivs B}
+  {F G : A -> B} `{!Is0Functor F, !Is0Functor G}
+  (alpha : NatTrans F G) `{forall a, CatIsEquiv (alpha a)}
+  : NatEquiv F G.
+Proof.
+  snapply Build_NatEquiv.
+  -
+ intro a.
+    exact (Build_CatEquiv (alpha a)).
+  -
+ snapply Build_Is1Natural'.
+    +
+ intros a a' f.
+      refine ((cate_buildequiv_fun _ $@R _) $@ _ $@ (_ $@L cate_buildequiv_fun _)^$).
+      exact (isnat alpha _).
+    +
+ intros a a' f.
+      refine ((_ $@L cate_buildequiv_fun _) $@ _ $@ (cate_buildequiv_fun _ $@R _)^$).
+      exact (isnat_tr alpha _).
+Defined.
+Definition natequiv_compose {A B} {F G H : A -> B} `{IsGraph A} `{HasEquivs B}
+  `{!Is0Functor F, !Is0Functor G, !Is0Functor H}
+  (alpha : NatEquiv G H) (beta : NatEquiv F G)
+  : NatEquiv F H.
+exact (Build_NatEquiv' (nattrans_comp alpha beta)).
+Defined.
+
+Definition natequiv_inverse {A B : Type} `{IsGraph A} `{HasEquivs B}
+  {F G : A -> B} `{!Is0Functor F, !Is0Functor G}
+  : NatEquiv F G -> NatEquiv G F.
+Proof.
+  intros [alpha I].
+  snapply Build_NatEquiv.
+  1: exact (fun a => (alpha a)^-1$).
+  snapply Build_Is1Natural'.
+  +
+ intros X Y f.
+    apply vinverse, I.
+  +
+ intros X Y f.
+    apply hinverse, I.
+Defined.
+
+Record Fun01 (A B : Type) `{IsGraph A} `{IsGraph B} := {
+  fun01_F : A -> B;
+  fun01_is0functor :: Is0Functor fun01_F;
+}.
+
+Coercion fun01_F : Fun01 >-> Funclass.
+
+Arguments Build_Fun01 {A B isgraph_A isgraph_B} F {fun01_is0functor} : rename.
+Arguments fun01_F {A B isgraph_A isgraph_B} : rename.
+Definition Build_Fun01' {A B : Type} `{IsGraph A} `{IsGraph B}
+  (F : A -> B) (fmap : forall a b (f : a $-> b), F a $-> F b)
+  : Fun01 A B.
+exact (Build_Fun01 F (fun01_is0functor:=Build_Is0Functor F fmap)).
+Defined.
+
+Instance isgraph_fun01 (A B : Type) `{IsGraph A} `{Is1Cat B} : IsGraph (Fun01 A B).
+Proof.
+  srapply Build_IsGraph.
+  intros [F ?] [G ?].
+  exact (NatTrans F G).
+Defined.
+
+Instance is01cat_fun01 (A B : Type) `{IsGraph A} `{Is1Cat B} : Is01Cat (Fun01 A B).
+Proof.
+  srapply Build_Is01Cat.
+  -
+ intros [F ?]; cbn.
+    exact (nattrans_id F).
+  -
+ intros F G K gamma alpha; cbn in *.
+    exact (nattrans_comp gamma alpha).
+Defined.
+
+Instance is2graph_fun01 (A B : Type) `{IsGraph A, Is1Cat B}
+  : Is2Graph (Fun01 A B).
+Proof.
+  intros [F ?] [G ?]; apply Build_IsGraph.
+  intros [alpha ?] [gamma ?].
+  exact (forall a, alpha a $== gamma a).
+Defined.
+
+Instance is1cat_fun01 (A B : Type) `{IsGraph A} `{Is1Cat B} : Is1Cat (Fun01 A B).
+Admitted.
+
+Instance hasequivs_fun01 (A B : Type) `{Is01Cat A} `{HasEquivs B}
+  : HasEquivs (Fun01 A B).
+Proof.
+  srapply Build_HasEquivs.
+  1: intros F G; exact (NatEquiv F G).
+  all: intros F G alpha; cbn in *.
+  -
+ exact (forall a, CatIsEquiv (alpha a)).
+  -
+ exact alpha.
+  -
+ intros a; exact _.
+  -
+ apply Build_NatEquiv'.
+  -
+ cbn; intros; apply cate_buildequiv_fun.
+  -
+ exact (natequiv_inverse alpha).
+  -
+ intros; apply cate_issect.
+  -
+ intros; apply cate_isretr.
+  -
+ intros [gamma ?] r s a; cbn in *.
+    exact (catie_adjointify (alpha a) (gamma a) (r a) (s a)).
+Defined.
+
+Record Fun11 (A B : Type) `{Is1Cat A} `{Is1Cat B} :=
+{
+  fun11_fun : A -> B ;
+  is0functor_fun11 :: Is0Functor fun11_fun ;
+  is1functor_fun11 :: Is1Functor fun11_fun
+}.
+
+Coercion fun11_fun : Fun11 >-> Funclass.
+
+Arguments Build_Fun11 A B
+  {isgraph_A is2graph_A is01cat_A is1cat_A
+   isgraph_B is2graph_B is01cat_B is1cat_B}
+  F {is0functor_fun11 is1functor_fun11} : rename.
+
+Coercion fun01_fun11 {A B : Type} `{Is1Cat A} `{Is1Cat B}
+           (F : Fun11 A B)
+  : Fun01 A B.
+Proof.
+  exists F; exact _.
+Defined.
+Instance isgraph_fun11 {A B : Type} `{Is1Cat A} `{Is1Cat B}
+  : IsGraph (Fun11 A B).
+exact (isgraph_induced fun01_fun11).
+Defined.
+Instance is01cat_fun11 {A B : Type} `{Is1Cat A} `{Is1Cat B}
+  : Is01Cat (Fun11 A B).
+exact (is01cat_induced fun01_fun11).
+Defined.
+Instance is2graph_fun11 {A B : Type} `{Is1Cat A, Is1Cat B}
+  : Is2Graph (Fun11 A B).
+exact (is2graph_induced fun01_fun11).
+Defined.
+Instance is1cat_fun11 {A B :Type} `{Is1Cat A} `{Is1Cat B}
+  : Is1Cat (Fun11 A B).
+exact (is1cat_induced fun01_fun11).
+Defined.
+Instance hasequivs_fun11 {A B : Type} `{Is1Cat A} `{HasEquivs B}
+  : HasEquivs (Fun11 A B).
+exact (hasequivs_induced fun01_fun11).
+Defined.
+Definition fun01_id {A} `{IsGraph A} : Fun01 A A.
+exact (Build_Fun01 idmap).
+Defined.
+Definition fun01_compose {A B C} `{IsGraph A, IsGraph B, IsGraph C}
+  : Fun01 B C -> Fun01 A B -> Fun01 A C.
+exact (fun G F => Build_Fun01 (G o F)).
+Defined.
+
+Record Graph := {
+  graph_carrier :> Type;
+  isgraph_graph_carrier :: IsGraph graph_carrier
+}.
+
+Instance isgraph_graph : IsGraph Graph
+  := { Hom A B := Fun01 A B }.
+Instance is2graph_graph : Is2Graph Graph.
+exact (fun A B => {| Hom F G := Transformation (fun01_F F) (fun01_F G) |}).
+Defined.
+
+Instance is01cat_graph : Is01Cat Graph := {
+  Id A := fun01_id;
+  cat_comp A B C G F := fun01_compose G F
+}.
+
+Scheme sum_rec := Minimality for sum Sort Type.
+Arguments sum_rec {A B} P f g s : rename.
+Instance isgraph_type@{u v} : IsGraph@{v u} Type@{u}.
+exact (Build_IsGraph Type@{u} (fun a b => a -> b)).
+Defined.
+
+Instance is01cat_type : Is01Cat Type.
+Proof.
+  econstructor.
+  +
+ intro; exact idmap.
+  +
+ exact (fun a b c g f => g o f).
+Defined.
+Instance is2graph_type : Is2Graph Type.
+exact (fun x y => Build_IsGraph _ (fun f g => f == g)).
+Defined.
+
+Instance is1cat_strong_type : Is1Cat_Strong Type.
+Admitted.
+
+Instance hasequivs_type : HasEquivs Type.
+Proof.
+  srefine (Build_HasEquivs Type _ _ _ _ Equiv (@IsEquiv) _ _ _ _ _ _ _ _); intros A B.
+  all:intros f.
+  -
+ exact f.
+  -
+ exact _.
+  -
+ apply Build_Equiv.
+  -
+ intros; reflexivity.
+  -
+ intros; exact (f^-1).
+  -
+ cbn.
+intros ?; apply eissect.
+  -
+ cbn.
+intros ?; apply eisretr.
+  -
+ intros g r s; exact (isequiv_adjointify f g r s).
+Defined.
+
+Record ZeroGpd := {
+  carrier :> Type;
+  isgraph_carrier :: IsGraph carrier;
+  is01cat_carrier :: Is01Cat carrier;
+  is0gpd_carrier :: Is0Gpd carrier;
+}.
+Definition zerogpd_graph (C : ZeroGpd) : Graph.
+exact ({|
+    graph_carrier := carrier C;
+    isgraph_graph_carrier := isgraph_carrier C
+  |}).
+Defined.
+Instance isgraph_0gpd : IsGraph ZeroGpd.
+exact (isgraph_induced zerogpd_graph).
+Defined.
+Instance is01cat_0gpd : Is01Cat ZeroGpd.
+exact (is01cat_induced zerogpd_graph).
+Defined.
+Instance is2graph_0gpd : Is2Graph ZeroGpd.
+exact (is2graph_induced zerogpd_graph).
+Defined.
+
+Instance is1cat_0gpd : Is1Cat ZeroGpd.
+Admitted.
+Instance hasequivs_0gpd : HasEquivs ZeroGpd.
+exact (cat_hasequivs ZeroGpd).
+Defined.
+ Section GraphQuotient.
+  Context {A : Type@{i}}.
+
+  Private Inductive GraphQuotient (R : A -> A -> Type@{j}) : Type@{u} :=
+  | gq : A -> GraphQuotient R.
+
+  Arguments gq {R} a.
+
+  Context {R : A -> A -> Type@{j}}.
+
+  Axiom gqglue : forall {a b : A},
+    R a b -> paths (@gq R a) (gq b).
+Definition GraphQuotient_ind
+    (P : GraphQuotient R -> Type@{k})
+    (gq' : forall a, P (gq a))
+    (gqglue' : forall a b (s : R a b), gqglue s # gq' a = gq' b)
+    : forall x, P x.
+exact (fun x =>
+    match x with
+    | gq a => fun _ => gq' a
+    end gqglue').
+Defined.
+
+  Axiom GraphQuotient_ind_beta_gqglue
+  : forall (P : GraphQuotient R -> Type@{k})
+    (gq' : forall a, P (gq a))
+    (gqglue' : forall a b (s : R a b), gqglue s # gq' a = gq' b)
+    (a b: A) (s : R a b),
+    apD (GraphQuotient_ind P gq' gqglue') (gqglue s) = gqglue' a b s.
+
+ End GraphQuotient.
+
+Arguments gq {A R} a.
+
+Definition GraphQuotient_rec {A R P} (c : A -> P) (g : forall a b, R a b -> c a = c b)
+  : GraphQuotient R -> P.
+Proof.
+  srapply GraphQuotient_ind.
+  1: exact c.
+  intros a b s.
+  exact (transport_const _ _ @ g a b s).
+Defined.
+
+Definition GraphQuotient_rec_beta_gqglue {A R P}
+  (c : A -> P) (g : forall a b, R a b -> c a = c b)
+  (a b : A) (s : R a b)
+  : ap (GraphQuotient_rec c g) (gqglue s) = g a b s.
+Proof.
+  unfold GraphQuotient_rec.
+  refine (cancelL _ _ _ _ ).
+  refine ((apD_const _ _)^ @ _).
+  rapply GraphQuotient_ind_beta_gqglue.
+Defined.
+Definition Coeq@{i j u} {B : Type@{i}} {A : Type@{j}} (f g : B -> A) : Type@{u}.
+exact (GraphQuotient@{i j u} (fun a b => {x : B & (f x = a) * (g x = b)})).
+Defined.
+Definition coeq {B A f g} (a : A) : @Coeq B A f g.
+exact (gq a).
+Defined.
+Definition cglue {B A f g} b : @coeq B A f g (f b) = coeq (g b).
+exact (gqglue (b; (idpath,idpath))).
+Defined.
+Arguments coeq : simpl never.
+
+Definition Coeq_ind {B A f g} (P : @Coeq B A f g -> Type)
+  (coeq' : forall a, P (coeq a))
+  (cglue' : forall b, (cglue b) # (coeq' (f b)) = coeq' (g b))
+  : forall w, P w.
+Proof.
+  rapply GraphQuotient_ind.
+  intros a b [x [[] []]].
+  exact (cglue' x).
+Defined.
+
+Definition Coeq_rec {B A f g} (P : Type) (coeq' : A -> P)
+  (cglue' : forall b, coeq' (f b) = coeq' (g b))
+  : @Coeq B A f g -> P.
+Proof.
+  rapply GraphQuotient_rec.
+  intros a b [x [[] []]].
+  exact (cglue' x).
+Defined.
+
+Definition Coeq_rec_beta_cglue {B A f g} (P : Type) (coeq' : A -> P)
+  (cglue' : forall b:B, coeq' (f b) = coeq' (g b)) (b:B)
+  : ap (Coeq_rec P coeq' cglue') (cglue b) = cglue' b.
+Proof.
+  rapply GraphQuotient_rec_beta_gqglue.
+Defined.
+Definition Pushout@{i j k l} {A : Type@{i}} {B : Type@{j}} {C : Type@{k}}
+  (f : A -> B) (g : A -> C) : Type@{l}.
+exact (Coeq@{l l _} (inl o f) (inr o g)).
+Defined.
+Definition push {A B C : Type} {f : A -> B} {g : A -> C}
+ : B+C -> Pushout f g.
+exact (@coeq _ _ (inl o f) (inr o g)).
+Defined.
+Definition pushl {A B C} {f : A -> B} {g : A -> C} (b : B)
+  : Pushout f g.
+exact (push (inl b)).
+Defined.
+Definition pushr {A B C} {f : A -> B} {g : A -> C} (c : C)
+  : Pushout f g.
+exact (push (inr c)).
+Defined.
+
+Definition pglue {A B C : Type} {f : A -> B} {g : A -> C} (a : A)
+  : pushl (f a) = pushr (g a)
+  := @cglue A (B+C) (inl o f) (inr o g) a.
+
+Section PushoutInd.
+
+  Context {A B C : Type} {f : A -> B} {g : A -> C}
+    (P : Pushout f g -> Type)
+    (pushb : forall b : B, P (pushl b))
+    (pushc : forall c : C, P (pushr c))
+    (pusha : forall a : A, (pglue a) # (pushb (f a)) = pushc (g a)).
+Definition Pushout_ind
+    : forall (w : Pushout f g), P w.
+exact (Coeq_ind P (sum_ind (P o push) pushb pushc) pusha).
+Defined.
+
+End PushoutInd.
+Definition Pushout_rec {A B C} {f : A -> B} {g : A -> C} (P : Type)
+  (pushb : B -> P)
+  (pushc : C -> P)
+  (pusha : forall a : A, pushb (f a) = pushc (g a))
+  : @Pushout A B C f g -> P.
+exact (@Coeq_rec _ _ (inl o f) (inr o g) P (sum_rec P pushb pushc) pusha).
+Defined.
+
+Definition Pushout_rec_beta_pglue {A B C f g} (P : Type)
+  (pushb : B -> P)
+  (pushc : C -> P)
+  (pusha : forall a : A, pushb (f a) = pushc (g a))
+  (a : A)
+  : ap (Pushout_rec P pushb pushc pusha) (pglue a) = pusha a.
+Proof.
+  napply Coeq_rec_beta_cglue.
+Defined.
+Definition opyon_0gpd {A : Type} `{Is1Cat A} (a : A) : A -> ZeroGpd.
+exact (fun b => Build_ZeroGpd (a $-> b) _ _ _).
+Defined.
+
+Instance is0functor_opyon_0gpd {A : Type} `{Is1Cat A} (a : A)
+  : Is0Functor (opyon_0gpd a).
+Proof.
+  apply Build_Is0Functor.
+  intros b c f.
+  exact (Build_Fun01 (cat_postcomp a f)).
+Defined.
+
+Instance is1functor_opyon_0gpd {A : Type} `{Is1Cat A} (a : A)
+  : Is1Functor (opyon_0gpd a).
+Admitted.
+
+Definition opyoneda_0gpd {A : Type} `{Is1Cat A} (a : A)
+           (F : A -> ZeroGpd) `{!Is0Functor F, !Is1Functor F}
+  : F a -> (opyon_0gpd a $=> F).
+Proof.
+  intros x b.
+  refine (Build_Fun01' (A:=opyon_0gpd a b) (B:=F b) (fun f => fmap F f x) _).
+  intros f1 f2 h.
+  exact (fmap2 F h x).
+Defined.
+Definition un_opyoneda_0gpd {A : Type} `{Is1Cat A}
+  (a : A) (F : A -> ZeroGpd) {ff : Is0Functor F}
+  : (opyon_0gpd a $=> F) -> F a.
+exact (fun alpha => alpha a (Id a)).
+Defined.
+
+Definition opyoneda_isretr_0gpd {A : Type} `{Is1Cat A} (a : A)
+  (F : A -> ZeroGpd) `{!Is0Functor F, !Is1Functor F}
+  (alpha : opyon_0gpd a $=> F) {alnat : Is1Natural (opyon_0gpd a) F alpha}
+  (b : A)
+  : opyoneda_0gpd a F (un_opyoneda_0gpd a F alpha) b $== alpha b.
+Admitted.
+Definition opyon1_0gpd {A : Type} `{Is1Cat A} (a : A) : Fun11 A ZeroGpd.
+exact (Build_Fun11 _ _ (opyon_0gpd a)).
+Defined.
+
+Definition opyon_equiv_0gpd {A : Type} `{HasEquivs A}
+  {a b : A} (f : opyon1_0gpd a $<~> opyon1_0gpd b)
+  : b $<~> a.
+Proof.
+
+  set (fa := (cate_fun f a) (Id a)).
+
+  set (gb := (cate_fun f^-1$ b) (Id b)).
+
+  srapply (cate_adjointify fa gb).
+
+  -
+ exact (opyoneda_isretr_0gpd _ _ f^-1$ a fa $@ cat_eissect (f a) (Id a)).
+  -
+ exact (opyoneda_isretr_0gpd _ _ f     b gb $@ cat_eisretr (f b) (Id b)).
+Defined.
+
+  Definition Join (A : Type@{i}) (B : Type@{j})
+    := Pushout@{k i j k} (@fst A B) (@snd A B).
+Definition joinl {A B} : A -> Join A B.
+exact (fun a => @pushl (A*B) A B fst snd a).
+Defined.
+Definition joinr {A B} : B -> Join A B.
+exact (fun b => @pushr (A*B) A B fst snd b).
+Defined.
+
+  Definition jglue {A B} a b : joinl a = joinr b
+    := @pglue (A*B) A B fst snd (a , b).
+
+  Definition Join_ind {A B : Type} (P : Join A B -> Type)
+    (P_A : forall a, P (joinl a)) (P_B : forall b, P (joinr b))
+    (P_g : forall a b, transport P (jglue a b) (P_A a) = P_B b)
+    : forall (x : Join A B), P x.
+  Proof.
+    apply (Pushout_ind P P_A P_B).
+    exact (fun ab => P_g (fst ab) (snd ab)).
+  Defined.
+
+  Definition Join_rec {A B P : Type} (P_A : A -> P) (P_B : B -> P)
+    (P_g : forall a b, P_A a = P_B b) : Join A B -> P.
+  Proof.
+    apply (Pushout_rec P P_A P_B).
+    exact (fun ab => P_g (fst ab) (snd ab)).
+  Defined.
+
+  Definition Join_rec_beta_jglue {A B P : Type} (P_A : A -> P)
+    (P_B : B -> P) (P_g : forall a b, P_A a = P_B b) a b
+    : ap (Join_rec P_A P_B P_g) (jglue a b) = P_g a b.
+  Proof.
+    exact (Pushout_rec_beta_pglue _ _ _ _ (a, b)).
+  Defined.
+
+Record JoinRecData {A B P : Type} := {
+    jl : A -> P;
+    jr : B -> P;
+    jg : forall a b, jl a = jr b;
+  }.
+
+Arguments JoinRecData : clear implicits.
+Arguments Build_JoinRecData {A B P}%_type_scope (jl jr jg)%_function_scope.
+Definition join_rec {A B P : Type} (f : JoinRecData A B P)
+  : Join A B $-> P.
+Admitted.
+
+Definition joinrecdata_fun {A B P Q : Type} (g : P -> Q) (f : JoinRecData A B P)
+  : JoinRecData A B Q.
+Proof.
+  snapply Build_JoinRecData.
+  -
+ exact (g o jl f).
+  -
+ exact (g o jr f).
+  -
+ exact (fun a b => ap g (jg f a b)).
+Defined.
+
+Record JoinRecPath {A B P : Type} {f g : JoinRecData A B P} := {
+    hl : forall a, jl f a = jl g a;
+    hr : forall b, jr f b = jr g b;
+    hg : forall a b, jg f a b @ hr b = hl a @ jg g a b;
+  }.
+
+Arguments JoinRecPath {A B P} f g.
+
+Definition bundle_joinrecpath {A B P : Type} {jl' : A -> P} {jr' : B -> P}
+  {f g : forall a b, jl' a = jr' b}
+  (h : forall a b, f a b = g a b)
+  : JoinRecPath (Build_JoinRecData jl' jr' f) (Build_JoinRecData jl' jr' g).
+Admitted.
+
+Ltac bundle_joinrecpath :=
+  hnf;
+  match goal with |- JoinRecPath ?F ?G =>
+    refine (bundle_joinrecpath (f:=jg F) (g:=jg G) _) end.
+
+Ltac generalize_three f a b :=
+  let fg := fresh in let fr := fresh in let fl := fresh in
+  destruct f as [fl fr fg]; cbn;
+  generalize (fg a b); clear fg;
+  generalize (fr b); clear fr;
+  generalize (fl a); clear fl.
+
+Ltac interval_ind f a b :=
+  generalize_three f a b;
+  intro f;
+  apply paths_ind.
+
+Definition square_ind {P : Type} (a b : P) (ab : a = b)
+  (Q : forall (a' b' : P) (ab' : a' = b') (ha : a = a') (hb : b = b') (k : ab @ hb = ha @ ab'), Type)
+  (s : Q a b ab idpath idpath (equiv_p1_1q idpath))
+  : forall a' b' ab' ha hb k, Q a' b' ab' ha hb k.
+Admitted.
+
+Global Ltac square_ind g h a b :=
+  generalize_three h a b;
+  generalize_three g a b;
+  apply square_ind.
+Instance isgraph_joinrecdata (A B P : Type) : IsGraph (JoinRecData A B P).
+exact ({| Hom := JoinRecPath |}).
+Defined.
+
+Instance is01cat_joinrecdata (A B P : Type) : Is01Cat (JoinRecData A B P).
+Admitted.
+
+Instance is0gpd_joinrecdata (A B P : Type) : Is0Gpd (JoinRecData A B P).
+Admitted.
+Definition joinrecdata_0gpd (A B P : Type) : ZeroGpd.
+exact (Build_ZeroGpd (JoinRecData A B P) _ _ _).
+Defined.
+
+Instance is0functor_joinrecdata_fun {A B P Q : Type} (g : P -> Q)
+  : Is0Functor (@joinrecdata_fun A B P Q g).
+Admitted.
+
+Instance is0functor_joinrecdata_0gpd (A B : Type) : Is0Functor (joinrecdata_0gpd A B).
+Proof.
+  apply Build_Is0Functor.
+  intros P Q g.
+  exact (Build_Fun01 (joinrecdata_fun g)).
+Defined.
+
+Instance is1functor_joinrecdata_0gpd (A B : Type) : Is1Functor (joinrecdata_0gpd A B).
+Admitted.
+Definition joinrecdata_0gpd_fun (A B : Type) : Fun11 Type ZeroGpd.
+exact (Build_Fun11 _ _ (joinrecdata_0gpd A B)).
+Defined.
+
+Definition join_rec_inv_natequiv (A B : Type)
+  : NatEquiv (opyon_0gpd (Join A B)) (joinrecdata_0gpd_fun A B).
+Admitted.
+
+Definition join_rec_natequiv (A B : Type)
+  := natequiv_inverse (join_rec_inv_natequiv A B).
+
+Section Triangle.
+
+  Context {A B : Type}.
+
+  Definition triangle_v (a : A) {b b' : B} (p : b = b')
+    : jglue a b @ ap joinr p = jglue a b'.
+Admitted.
+
+End Triangle.
+Definition functor_join {A B C D} (f : A -> C) (g : B -> D)
+    : Join A B -> Join C D.
+Admitted.
+
+  #[export] Instance isequiv_functor_join {A B C D}
+    (f : A -> C) `{!IsEquiv f} (g : B -> D) `{!IsEquiv g}
+    : IsEquiv (functor_join f g).
+Admitted.
+Definition equiv_functor_join {A B C D} (f : A <~> C) (g : B <~> D)
+    : Join A B <~> Join C D.
+exact (Build_Equiv _ _ (functor_join f g) _).
+Defined.
+
+  Definition joinrecdata_sym (A B P : Type)
+    : joinrecdata_0gpd A B P $-> joinrecdata_0gpd B A P.
+  Proof.
+    snapply Build_Fun01'.
+
+    -
+ intros [fl fr fg].
+      snapply (Build_JoinRecData fr fl).
+      intros b a; exact (fg a b)^.
+
+    -
+ intros f g h; simpl.
+      snapply Build_JoinRecPath; simpl.
+      1, 2: intros; apply h.
+      intros b a.
+      square_ind g h a b.
+      by interval_ind f a b.
+  Defined.
+
+  Definition joinrecdata_sym_inv (A B P : Type)
+    : joinrecdata_sym B A P $o joinrecdata_sym A B P $== Id _.
+Admitted.
+
+  Definition joinrecdata_sym_natequiv (A B : Type)
+    : NatEquiv (joinrecdata_0gpd_fun A B) (joinrecdata_0gpd_fun B A).
+  Proof.
+    snapply Build_NatEquiv.
+
+    -
+ intro P.
+      snapply cate_adjointify.
+      1, 2: apply joinrecdata_sym.
+      1, 2: apply joinrecdata_sym_inv.
+
+    -
+ snapply Build_Is1Natural.
+      intros P Q g f; simpl.
+      bundle_joinrecpath.
+      intros b a; simpl.
+      symmetry; apply ap_V.
+  Defined.
+Definition joinrecdata_fun_sym (A B : Type)
+    : NatEquiv (opyon_0gpd (Join A B)) (opyon_0gpd (Join B A)).
+exact (natequiv_compose (join_rec_natequiv B A)
+        (natequiv_compose (joinrecdata_sym_natequiv A B) (join_rec_inv_natequiv A B))).
+Defined.
+
+  Definition equiv_join_sym' (A B : Type)
+    : Join A B <~> Join B A.
+  Proof.
+    tapply (opyon_equiv_0gpd (A:=Type)).
+    apply joinrecdata_fun_sym.
+  Defined.
+Definition join_sym_recdata (A B : Type)
+    : JoinRecData A B (Join B A).
+exact (Build_JoinRecData joinr joinl (fun a b => (jglue b a)^)).
+Defined.
+Definition join_sym (A B : Type)
+    : Join A B -> Join B A.
+exact (join_rec (join_sym_recdata A B)).
+Defined.
+
+  Definition join_sym_homotopic (A B : Type)
+    : join_sym A B == equiv_join_sym' A B.
+Admitted.
+Definition equiv_join_sym (A B : Type) : Join A B <~> Join B A.
+exact (equiv_homotopic_inverse (equiv_join_sym' A B)
+                              (join_sym_homotopic A B)
+                              (join_sym_homotopic B A)).
+Defined.
+
+Section TriJoinStructure.
+  Context {A B C : Type}.
+
+  Definition TriJoin := Join A (Join B C).
+Definition join1 : A -> TriJoin.
+exact (joinl).
+Defined.
+Definition join2 : B -> TriJoin.
+exact (fun b => (joinr (joinl b))).
+Defined.
+Definition join3 : C -> TriJoin.
+exact (fun c => (joinr (joinr c))).
+Defined.
+Definition join12 : forall a b, join1 a = join2 b.
+exact (fun a b => jglue a (joinl b)).
+Defined.
+Definition join13 : forall a c, join1 a = join3 c.
+exact (fun a c => jglue a (joinr c)).
+Defined.
+Definition join23 : forall b c, join2 b = join3 c.
+exact (fun b c => ap joinr (jglue b c)).
+Defined.
+End TriJoinStructure.
+
+Arguments TriJoin A B C : clear implicits.
+Definition ap_triangle {X Y} (f : X -> Y)
+  {a b c : X} {ab : a = b} {bc : b = c} {ac : a = c} (abc : ab @ bc = ac)
+  : ap f ab @ ap f bc = ap f ac.
+Admitted.
+
+Definition ap_trijoin {A B C P : Type} (f : TriJoin A B C -> P)
+  (a : A) (b : B) (c : C)
+  : ap f (join12 a b) @ ap f (join23 b c) = ap f (join13 a c).
+Admitted.
+
+Definition ap_trijoin_V {A B C P : Type} (f : TriJoin A B C -> P)
+  (a : A) (b : B) (c : C)
+  : ap_triangle f (triangle_v a (jglue b c)^)
+     = (1 @@ (ap (ap f) (ap_V joinr _) @ ap_V f _)) @ moveR_pV _ _ _ (ap_trijoin f a b c)^.
+Admitted.
+
+Record TriJoinRecData {A B C P : Type} := {
+    j1 : A -> P;
+    j2 : B -> P;
+    j3 : C -> P;
+    j12 : forall a b, j1 a = j2 b;
+    j13 : forall a c, j1 a = j3 c;
+    j23 : forall b c, j2 b = j3 c;
+    j123 : forall a b c, j12 a b @ j23 b c = j13 a c;
+  }.
+
+Arguments TriJoinRecData : clear implicits.
+Arguments Build_TriJoinRecData {A B C P}%_type_scope (j1 j2 j3 j12 j13 j23 j123)%_function_scope.
+
+Definition trijoin_rec {A B C P : Type} (f : TriJoinRecData A B C P)
+  : TriJoin A B C $-> P.
+Proof.
+  snapply Join_rec.
+  -
+ exact (j1 f).
+  -
+ snapply Join_rec.
+    +
+ exact (j2 f).
+    +
+ exact (j3 f).
+    +
+ exact (j23 f).
+  -
+ intro a.
+    snapply Join_ind; cbn beta.
+    +
+ exact (j12 f a).
+    +
+ exact (j13 f a).
+    +
+ intros b c.
+      lhs napply transport_paths_Fr.
+      exact (1 @@ Join_rec_beta_jglue _ _ _ _ _ @ j123 f a b c).
+Defined.
+Definition trijoin_rec_beta_join12 {A B C P : Type} (f : TriJoinRecData A B C P) (a : A) (b : B)
+  : ap (trijoin_rec f) (join12 a b) = j12 f a b.
+exact (Join_rec_beta_jglue _ _ _ _ _).
+Defined.
+Definition trijoin_rec_beta_join13 {A B C P : Type} (f : TriJoinRecData A B C P) (a : A) (c : C)
+  : ap (trijoin_rec f) (join13 a c) = j13 f a c.
+Admitted.
+
+Definition trijoin_rec_beta_join23 {A B C P : Type} (f : TriJoinRecData A B C P) (b : B) (c : C)
+  : ap (trijoin_rec f) (join23 b c) = j23 f b c.
+Admitted.
+
+Definition trijoin_rec_beta_join123 {A B C P : Type} (f : TriJoinRecData A B C P)
+  (a : A) (b : B) (c : C)
+  : ap_trijoin (trijoin_rec f) a b c
+    = (trijoin_rec_beta_join12 f a b @@ trijoin_rec_beta_join23 f b c)
+        @ j123 f a b c @ (trijoin_rec_beta_join13 f a c)^.
+Admitted.
+
+Definition trijoinrecdata_fun {A B C P Q : Type} (g : P -> Q) (f : TriJoinRecData A B C P)
+  : TriJoinRecData A B C Q.
+Proof.
+  snapply Build_TriJoinRecData.
+  -
+ exact (g o j1 f).
+  -
+ exact (g o j2 f).
+  -
+ exact (g o j3 f).
+  -
+ exact (fun a b => ap g (j12 f a b)).
+  -
+ exact (fun a c => ap g (j13 f a c)).
+  -
+ exact (fun b c => ap g (j23 f b c)).
+  -
+ intros a b c; cbn beta.
+    exact (ap_triangle g (j123 f a b c)).
+
+Defined.
+
+Definition prism {P : Type}
+  {a b c : P} {ab : a = b} {ac : a = c} {bc : b = c} (abc : ab @ bc = ac)
+  {a' b' c' : P} {ab' : a' = b'} {ac' : a' = c'} {bc' : b' = c'} (abc' : ab' @ bc' = ac')
+  {k1 : a = a'} {k2 : b = b'} {k3 : c = c'}
+  (k12 : ab @ k2 = k1 @ ab') (k13 : ac @ k3 = k1 @ ac') (k23 : bc @ k3 = k2 @ bc')
+  := concat_p_pp _ _ _ @ whiskerR abc k3 @ k13
+    = whiskerL ab k23
+    @ concat_p_pp _ _ _ @ whiskerR k12 bc'
+    @ concat_pp_p _ _ _ @ whiskerL k1 abc'.
+
+Record TriJoinRecPath {A B C P : Type} {f g : TriJoinRecData A B C P} := {
+    h1 : forall a, j1 f a = j1 g a;
+    h2 : forall b, j2 f b = j2 g b;
+    h3 : forall c, j3 f c = j3 g c;
+    h12 : forall a b, j12 f a b @ h2 b = h1 a @ j12 g a b;
+    h13 : forall a c, j13 f a c @ h3 c = h1 a @ j13 g a c;
+    h23 : forall b c, j23 f b c @ h3 c = h2 b @ j23 g b c;
+    h123 : forall a b c, prism (j123 f a b c) (j123 g a b c) (h12 a b) (h13 a c) (h23 b c);
+  }.
+
+Arguments TriJoinRecPath {A B C P} f g.
+
+Record TriJoinRecData' {A B C P : Type} {j1' : A -> P} {j2' : B -> P} {j3' : C -> P} := {
+    j12' : forall a b, j1' a = j2' b;
+    j13' : forall a c, j1' a = j3' c;
+    j23' : forall b c, j2' b = j3' c;
+    j123' : forall a b c, j12' a b @ j23' b c = j13' a c;
+  }.
+
+Arguments TriJoinRecData' {A B C P} j1' j2' j3'.
+Arguments Build_TriJoinRecData' {A B C P}%_type_scope
+  (j1' j2' j3' j12' j13' j23' j123')%_function_scope.
+
+Definition prism' {P : Type} {a b c : P}
+  {ab : a = b} {ac : a = c} {bc : b = c} (abc : ab @ bc = ac)
+  {ab' : a = b} {ac' : a = c} {bc' : b = c} (abc' : ab' @ bc' = ac')
+  (k12 : ab = ab') (k13 : ac = ac') (k23 : bc = bc')
+  := abc @ k13 = (k12 @@ k23) @ abc'.
+
+Record TriJoinRecPath' {A B C P : Type} {j1' : A -> P} {j2' : B -> P} {j3' : C -> P}
+  {f g : TriJoinRecData' j1' j2' j3'} := {
+    h12' : forall a b, j12' f a b = j12' g a b;
+    h13' : forall a c, j13' f a c = j13' g a c;
+    h23' : forall b c, j23' f b c = j23' g b c;
+    h123' : forall a b c, prism' (j123' f a b c) (j123' g a b c) (h12' a b) (h13' a c) (h23' b c);
+  }.
+
+Arguments TriJoinRecPath' {A B C P} {j1' j2' j3'} f g.
+Definition bundle_trijoinrecdata {A B C P : Type} {j1' : A -> P} {j2' : B -> P} {j3' : C -> P}
+  (f : TriJoinRecData' j1' j2' j3')
+  : TriJoinRecData A B C P.
+exact (Build_TriJoinRecData j1' j2' j3' (j12' f) (j13' f) (j23' f) (j123' f)).
+Defined.
+Definition unbundle_trijoinrecdata {A B C P : Type} (f : TriJoinRecData A B C P)
+  : TriJoinRecData' (j1 f) (j2 f) (j3 f).
+exact (Build_TriJoinRecData' (j1 f) (j2 f) (j3 f) (j12 f) (j13 f) (j23 f) (j123 f)).
+Defined.
+
+Definition bundle_trijoinrecpath {A B C P : Type} {j1' : A -> P} {j2' : B -> P} {j3' : C -> P}
+  {f g : TriJoinRecData' j1' j2' j3'} (h : TriJoinRecPath' f g)
+  : TriJoinRecPath (bundle_trijoinrecdata f) (bundle_trijoinrecdata g).
+Admitted.
+
+Ltac bundle_trijoinrecpath :=
+  hnf;
+  match goal with |- TriJoinRecPath ?F ?G =>
+    refine (bundle_trijoinrecpath (f:=unbundle_trijoinrecdata F)
+                                  (g:=unbundle_trijoinrecdata G) _) end;
+  snapply Build_TriJoinRecPath'.
+Instance isgraph_trijoinrecdata (A B C P : Type) : IsGraph (TriJoinRecData A B C P).
+exact ({| Hom := TriJoinRecPath |}).
+Defined.
+
+Instance is0functor_trijoin_rec (A B C P : Type) : Is0Functor (@trijoin_rec A B C P).
+Admitted.
+
+Definition trijoin_rec_nat (A B C : Type) {P Q : Type} (g : P -> Q)
+  (f : TriJoinRecData A B C P)
+  : trijoin_rec (trijoinrecdata_fun g f) $== g o trijoin_rec f.
+Admitted.
+
+Definition functor_join_join_rec {A B C A' P} (f : A -> A') (g : JoinRecData B C P)
+  : functor_join f (join_rec g)
+    == trijoin_rec {| j1 := joinl o f; j2 := joinr o jl g; j3 := joinr o jr g;
+                      j12 := fun a b => jglue (f a) (jl g b);
+                      j13 := fun a c => jglue (f a) (jr g c);
+                      j23 := fun b c => ap joinr (jg g b c);
+                      j123 := fun a b c => triangle_v (f a) (jg g b c); |}.
+Admitted.
+Definition trijoin_id_sym A B C : TriJoin A B C <~> TriJoin A C B.
+exact (equiv_functor_join equiv_idmap (equiv_join_sym B C)).
+Defined.
+
+Definition trijoinrecdata_id_sym {A B C P} (f : TriJoinRecData A B C P)
+  : TriJoinRecData A C B P.
+Proof.
+  snapply (Build_TriJoinRecData (j1 f) (j3 f) (j2 f)); intros.
+  -
+ apply (j13 f).
+  -
+ apply (j12 f).
+  -
+ symmetry; apply (j23 f).
+  -
+ cbn beta.
+ apply moveR_pV; symmetry.
+    apply (j123 f).
+Defined.
+
+Definition trijoin_rec_id_sym {A B C P} (f : TriJoinRecData A C B P)
+  : trijoin_rec f o trijoin_id_sym A B C == trijoin_rec (trijoinrecdata_id_sym f).
+Proof.
+
+  etransitivity.
+  {
+ refine (cat_postwhisker (A:=Type) (trijoin_rec f) _).
+    apply functor_join_join_rec.
+}
+  unfold join_sym_recdata, jl, jr, jg.
+
+  refine ((trijoin_rec_nat A B C (trijoin_rec f) _)^$ $@ _).
+  refine (fmap trijoin_rec _).
+
+  bundle_trijoinrecpath; intros; cbn.
+  -
+ apply trijoin_rec_beta_join13.
+  -
+ apply trijoin_rec_beta_join12.
+  -
+ lhs refine (ap _ (ap_V _ _)).
+    lhs refine (ap_V (trijoin_rec f) _).
+    apply (ap inverse).
+    apply trijoin_rec_beta_join23.
+  -
+ unfold prism'.
+    rewrite ap_trijoin_V.
+    rewrite trijoin_rec_beta_join123.
+    set (f' := f).
+    destruct f as [f1 f2 f3 f12 f13 f23 f123].
+    Instructions cbn.
+    Timeout 1 cbn.
+Abort.
diff --git a/test-suite/success/cbn_perf.v b/test-suite/success/cbn_perf.v
new file mode 100644
index 000000000000..a503322c2eb1
--- /dev/null
+++ b/test-suite/success/cbn_perf.v
@@ -0,0 +1,287 @@
+(* -*- mode: coq; coq-prog-args: ("-allow-rewrite-rules") -*- *)
+
+(* Performance probes for the closure-based [cbn] implementation.
+
+   Each block below isolates one performance hazard from [ppedrot-cbn.md].
+   The [Instructions] prefix records a machine-independent-ish instruction
+   count in the test log.  The parameter sweeps are deliberately small enough
+   for the success suite, but they vary the dimensions that should distinguish
+   the desired complexity from the bad one called out in the review. *)
+
+Ltac mk_nat n :=
+  lazymatch n with
+  | O => constr:(O)
+  | S ?n' => let t := mk_nat n' in constr:(S t)
+  end.
+
+Ltac mk_nat_fun n :=
+  lazymatch n with
+  | O => constr:(fun x : nat => x)
+  | S ?n' =>
+    let f := mk_nat_fun n' in
+    constr:(fun x : nat => S (f x))
+  end.
+
+Ltac setup_nat_goal t := enough (t = O) by exact I.
+
+(* 1. Deep beta/zeta chains where a large argument is threaded but never
+      inspected.  Desired scaling is mainly in [fuel]; repeated eager
+      substitution/lifting shows up as dependence on [arg_size * fuel]. *)
+Fixpoint beta_zeta_chain (fuel : nat) (x : nat) : nat :=
+  match fuel with
+  | O => O
+  | S fuel' => (fun y : nat => let z := y in beta_zeta_chain fuel' z) x
+  end.
+
+Goal True.
+Proof.
+  let big := mk_nat 50 in setup_nat_goal constr:(beta_zeta_chain 20 big).
+  Instructions cbn.
+Abort.
+
+Goal True.
+Proof.
+  let big := mk_nat 100 in setup_nat_goal constr:(beta_zeta_chain 20 big).
+  Instructions cbn.
+Abort.
+
+Goal True.
+Proof.
+  let big := mk_nat 100 in setup_nat_goal constr:(beta_zeta_chain 40 big).
+  Instructions cbn.
+Abort.
+
+(* 2. Recursive fixpoints carrying a large invariant parameter.  The review
+      predicts bad behaviour when refolding forces that parameter at each
+      recursive step, i.e. roughly [param_size * fuel]. *)
+Fixpoint carry_invariant (big fuel : nat) : nat :=
+  match fuel with
+  | O => O
+  | S fuel' => carry_invariant big fuel'
+  end.
+
+Goal True.
+Proof.
+  let big := mk_nat 50 in setup_nat_goal constr:(carry_invariant big 30).
+  Instructions cbn.
+Abort.
+
+Goal True.
+Proof.
+  let big := mk_nat 100 in setup_nat_goal constr:(carry_invariant big 30).
+  Instructions cbn.
+Abort.
+
+Goal True.
+Proof.
+  let big := mk_nat 100 in setup_nat_goal constr:(carry_invariant big 60).
+  Instructions cbn.
+Abort.
+
+CoInductive stream : Set :=
+| scons : nat -> stream -> stream.
+
+CoFixpoint cofix_carry (big : nat) : stream := scons O (cofix_carry big).
+
+Fixpoint nth_stream (fuel : nat) (s : stream) : nat :=
+  match fuel with
+  | O => match s with scons n _ => n end
+  | S fuel' => match s with scons _ tail => nth_stream fuel' tail end
+  end.
+
+Goal True.
+Proof.
+  let big := mk_nat 50 in setup_nat_goal constr:(nth_stream 30 (cofix_carry big)).
+  Instructions cbn.
+Abort.
+
+Goal True.
+Proof.
+  let big := mk_nat 100 in setup_nat_goal constr:(nth_stream 30 (cofix_carry big)).
+  Instructions cbn.
+Abort.
+
+(* 3. Equality/progress checks on delayed closures.  [simpl nomatch] exercises
+      the path that compares pre- and post-unfolding states to decide whether
+      progress was made.  Re-forcing an unused large parameter gives the same
+      [param_size * fuel] signature. *)
+Fixpoint nomatch_progress (fuel : nat) (big : nat) (b : bool) : bool :=
+  match fuel with
+  | O => if b then true else false
+  | S fuel' => nomatch_progress fuel' big b
+  end.
+Arguments nomatch_progress : simpl nomatch.
+
+Goal True.
+Proof.
+  let big := mk_nat 50 in
+  enough (forall b : bool, nomatch_progress 30 big b = b) by exact I.
+  Instructions cbn.
+Abort.
+
+Goal True.
+Proof.
+  let big := mk_nat 100 in
+  enough (forall b : bool, nomatch_progress 30 big b = b) by exact I.
+  Instructions cbn.
+Abort.
+
+Goal True.
+Proof.
+  let big := mk_nat 100 in
+  enough (forall b : bool, nomatch_progress 60 big b = b) by exact I.
+  Instructions cbn.
+Abort.
+
+(* 4. Recursion over constructors with unused fields.  The payloads contain a
+      delayed substitution for [x]; [walk] only follows tails.  Internal stack
+      zipping that materializes constructor fields makes the instruction count
+      depend on [payload_size * length]. *)
+Inductive cell : Set :=
+| stop : cell
+| node : nat -> cell -> cell.
+
+Fixpoint walk (c : cell) : nat :=
+  match c with
+  | stop => O
+  | node _ tail => walk tail
+  end.
+
+Ltac mk_cell_fun len payload_size :=
+  lazymatch len with
+  | O => constr:(fun x : nat => stop)
+  | S ?len' =>
+    let payload := mk_nat_fun payload_size in
+    let tail := mk_cell_fun len' payload_size in
+    constr:(fun x : nat => node (payload x) (tail x))
+  end.
+
+Goal True.
+Proof.
+  let big := mk_nat 20 in
+  let c := mk_cell_fun 20 20 in
+  setup_nat_goal constr:(walk (c big)).
+  Instructions cbn.
+Abort.
+
+Goal True.
+Proof.
+  let big := mk_nat 20 in
+  let c := mk_cell_fun 20 40 in
+  setup_nat_goal constr:(walk (c big)).
+  Instructions cbn.
+Abort.
+
+Goal True.
+Proof.
+  let big := mk_nat 20 in
+  let c := mk_cell_fun 40 40 in
+  setup_nat_goal constr:(walk (c big)).
+  Instructions cbn.
+Abort.
+
+(* 5. Strong [cbn] over stuck case/fix structures with delayed components.
+      Failed refolding should not first force a raw structure and then traverse
+      the original delayed components again. *)
+Definition stuck_case (branch x : nat) : nat :=
+  (fun y : nat => match x with O => y | S _ => y end) branch.
+
+Goal True.
+Proof.
+  let branch := mk_nat 50 in
+  enough (forall x : nat, stuck_case branch x = stuck_case branch x) by exact I.
+  Instructions cbn.
+Abort.
+
+Goal True.
+Proof.
+  let branch := mk_nat 100 in
+  enough (forall x : nat, stuck_case branch x = stuck_case branch x) by exact I.
+  Instructions cbn.
+Abort.
+
+Goal True.
+Proof.
+  let branch := mk_nat 200 in
+  enough (forall x : nat, stuck_case branch x = stuck_case branch x) by exact I.
+  Instructions cbn.
+Abort.
+
+Goal True.
+Proof.
+  let branch := mk_nat 50 in
+  enough (((fun y : nat =>
+              (fix stuck_fix (n : nat) : nat :=
+                 match n with O => y | S n' => stuck_fix n' end)) branch)
+          = ((fun y : nat =>
+                (fix stuck_fix (n : nat) : nat :=
+                   match n with O => y | S n' => stuck_fix n' end)) branch)) by exact I.
+  Instructions cbn.
+Abort.
+
+Goal True.
+Proof.
+  let branch := mk_nat 100 in
+  enough (((fun y : nat =>
+              (fix stuck_fix (n : nat) : nat :=
+                 match n with O => y | S n' => stuck_fix n' end)) branch)
+          = ((fun y : nat =>
+                (fix stuck_fix (n : nat) : nat :=
+                   match n with O => y | S n' => stuck_fix n' end)) branch)) by exact I.
+  Instructions cbn.
+Abort.
+
+(* 6. Rewrite-rule reduction still forces candidate arguments eagerly.  The
+      first rule fails and the second succeeds, so a delayed [S big] argument
+      is a direct probe of the eager matching path. *)
+#[unfold_fix] Symbol rw_head : nat -> nat.
+Rewrite Rules rw_head_rew :=
+| rw_head O => O
+| rw_head (S ?n) => O.
+
+Goal True.
+Proof.
+  let big := mk_nat 50 in setup_nat_goal constr:((fun y : nat => rw_head y) (S big)).
+  Instructions cbn.
+Abort.
+
+Goal True.
+Proof.
+  let big := mk_nat 100 in setup_nat_goal constr:((fun y : nat => rw_head y) (S big)).
+  Instructions cbn.
+Abort.
+
+Goal True.
+Proof.
+  let big := mk_nat 200 in setup_nat_goal constr:((fun y : nat => rw_head y) (S big)).
+  Instructions cbn.
+Abort.
+
+(* 7. Local definition unfolding under binders.  The local let is outside the
+      products but used below them; eager lifting traverses the large body when
+      the local definition is unfolded in that deeper context. *)
+Goal True.
+Proof.
+  let big := mk_nat 100 in
+  enough (let local_big := big in forall a b c d : nat,
+    (match local_big with O => O | S _ => O end) = O) by exact I.
+  Instructions cbn.
+Abort.
+
+Goal True.
+Proof.
+  let big := mk_nat 100 in
+  enough (let local_big := big in forall a b c d : nat,
+    (match local_big with O => O | S _ => O end) +
+    (match local_big with O => O | S _ => O end) = O) by exact I.
+  Instructions cbn.
+Abort.
+
+Goal True.
+Proof.
+  let big := mk_nat 200 in
+  enough (let local_big := big in forall a b c d : nat,
+    (match local_big with O => O | S _ => O end) +
+    (match local_big with O => O | S _ => O end) = O) by exact I.
+  Instructions cbn.
+Abort.