FrameCompatibility.v

From Stdlib Require Import Arith Bool Lia Relations.Relation_Operators.
Require Import AdministrativeReduction.
Require Import AdministrativeAlgebra.
Require Import AdministrativeResiduals.
Require Import SharedPrompts.CoreAlgebra.
Require Import SharedPrompts.ScopedFusion.

Import SharedPrompts.

(* Canonical right-associated spines are derived gadgets for the mode
 relation. They are useful when a continuation replacement swallows the
 delimiter at the head of a tail: first expose all ordinary LetLet redexes,
 then contract the bottom LetS. *)
Fixpoint admin_let_assoc_spine (l : lctx) (q t : expr) : expr :=
 match l with
 | LNil => ELet q t
 | LLet a l' => ELet a (admin_let_assoc_spine l' q (olift_e 1 1 t))
 end.

Lemma admin_let_assoc_spine_star (l : lctx) (q t : expr) :
 star (admin_step)
 (ELet (plug_l l q) t)
 (admin_let_assoc_spine l q t).
Proof.
 revert q t.
 induction l as [|a l IH]; intros q t.
 - apply star_refl.
 - simpl.
 eapply star_step.
 + apply AS_LetAssoc.
 + apply (admin_star_map (admin_step) (admin_step)
 (fun z => ELet a z)).
 * intros x y Hxy. apply AS_LetBody. exact Hxy.
 * apply IH.
Qed.

Fixpoint admin_let_shift_spine (l : lctx) (e t : expr) : expr :=
 match l with
 | LNil => EShift (krepl_e 0 (frame t) e)
 | LLet a l' => ELet a (admin_let_shift_spine l' e (olift_e 1 1 t))
 end.

Lemma admin_let_shift_spine_star (l : lctx) (e t : expr) :
 star (admin_step)
 (ELet (plug_l l (EShift e)) t)
 (admin_let_shift_spine l e t).
Proof.
 revert e t.
 induction l as [|a l IH]; intros e t.
 - apply star_one. apply AS_LetShift.
 - simpl.
 eapply star_step.
 + apply AS_LetAssoc.
 + apply (admin_star_map (admin_step) (admin_step)
 (fun z => ELet a z)).
 * intros x y Hxy. apply AS_LetBody. exact Hxy.
 * apply IH.
Qed.

Fixpoint admin_spine_tail_lift (l : lctx) (q : expr) : expr :=
 match l with
 | LNil => q
 | LLet _ l' => admin_spine_tail_lift l' (olift_e 1 1 q)
 end.

Lemma admin_let_assoc_spine_tail_shape (l : lctx) (e q : expr) :
 admin_let_assoc_spine l e q =
 plug_l l (ELet e (admin_spine_tail_lift l q)).
Proof.
 revert e q.
 induction l as [|a l IH]; intros e q; simpl.
 - reflexivity.
 - rewrite (IH e (olift_e 1 1 q)). reflexivity.
Qed.

Lemma admin_let_shift_spine_abort_shape (l : lctx) (e q : expr) :
 admin_let_shift_spine l (klift_e 0 1 e) q =
 plug_l l (abort e).
Proof.
 revert e q.
 induction l as [|a l IH]; intros e q.
 - simpl.
 rewrite (proj2 admin_krepl_no_cocc
 (klift_e 0 1 e) 0 (frame q)).
 + reflexivity.
 + apply cocc_klift_fresh_e.
 - simpl. rewrite (IH e (olift_e 1 1 q)). reflexivity.
Qed.

Lemma admin_abort_tail_spine (h : nat) (l : lctx) (e q : expr) :
 joinable (admin_step)
 (ECont h
 (ELet (plug_l l
 (abort (ECont h (ELet e (admin_spine_tail_lift l q))))) q))
 (ECont h (ELet (plug_l l e) q)).
Proof.
 exists (ECont h (plug_l l (ELet e (admin_spine_tail_lift l q)))); split.
 - eapply star_trans.
 + apply (admin_star_map (admin_step) (admin_step) (ECont h)).
 * intros x y Hxy. apply AS_ContBody. exact Hxy.
 * apply (admin_let_shift_spine_star l
 (klift_e 0 1 (ECont h
 (ELet e (admin_spine_tail_lift l q)))) q).
 + rewrite (admin_let_shift_spine_abort_shape l
 (ECont h (ELet e (admin_spine_tail_lift l q))) q).
 apply star_one. apply AS_ContTail.
 apply tail_step_plug_abort.
 - eapply (admin_star_map (admin_step) (admin_step) (ECont h)).
 + intros x y Hxy. apply AS_ContBody. exact Hxy.
 + rewrite <- (admin_let_assoc_spine_tail_shape l e q).
 apply (admin_let_assoc_spine_star l e q).
Qed.

Lemma admin_krepl_installed_frame_abort_shape (h : nat) (q e : expr) :
 krepl_e h (installed_let_frame h q) (abort (ECont h e)) =
 abort (plug_d (installed_let_frame h q)
 (krepl_e h (installed_let_frame h q) e)).
Proof.
 unfold abort. simpl.
 replace (h + 1) with (S h) by lia.
 rewrite Nat.eqb_refl.
 assert (Hframe :
 klift_d 0 1 (installed_let_frame h q) =
 installed_let_frame (S h) (klift_e 0 1 q)).
 { unfold installed_let_frame, klift_d. simpl.
 destruct (Nat.leb 0 h); f_equal; lia. }
 repeat f_equal.
 assert (Hinst : ICont (S h) (CLet CHole (klift_e 0 1 q)) =
 klift_d 0 1 (installed_let_frame h q)).
 { change (installed_let_frame (S h) (klift_e 0 1 q) =
 klift_d 0 1 (installed_let_frame h q)).
 symmetry. exact Hframe. }
 rewrite Hinst.
 symmetry. apply admin_klift_krepl_e.
Qed.

Lemma admin_krepl_installed_frame_tail_abort_shape (h : nat) (q : expr)
 (l : lctx) (e : expr) :
 exists l' ep,
 krepl_e h (installed_let_frame h q)
 (plug_l l (abort (ECont h e))) =
 plug_l l'
 (abort (ECont h
 (ELet ep (admin_spine_tail_lift l' q)))) /\
 krepl_e h (installed_let_frame h q) (plug_l l e) = plug_l l' ep.
Proof.
 revert q e.
 induction l as [|a l IH]; intros q e.
 - exists LNil, (krepl_e h (installed_let_frame h q) e). split.
 + change (krepl_e h (installed_let_frame h q)
 (abort (ECont h e)) =
 abort (ECont h
 (ELet (krepl_e h (installed_let_frame h q) e) q))).
 rewrite admin_krepl_installed_frame_abort_shape.
 reflexivity.
 + reflexivity.
 - destruct (IH (olift_e 1 1 q) e)
 as [l' [ep [Ha Hb]]].
 exists (LLet (krepl_e h (installed_let_frame h q) a) l'), ep. split.
 + simpl.
 change (ELet (krepl_e h (installed_let_frame h q) a)
 (krepl_e h (olift_d 0 1 (installed_let_frame h q))
 (plug_l l (abort (ECont h e)))) =
 ELet (krepl_e h (installed_let_frame h q) a)
 (plug_l l'
 (abort (ECont h
 (ELet ep (admin_spine_tail_lift l'
 (olift_e 1 1 q))))))).
 rewrite (admin_olift_installed_let_frame 0 1 h q), Ha.
 reflexivity.
 + simpl.
 change (ELet (krepl_e h (installed_let_frame h q) a)
 (krepl_e h (olift_d 0 1 (installed_let_frame h q))
 (plug_l l e)) =
 ELet (krepl_e h (installed_let_frame h q) a)
 (plug_l l' ep)).
 rewrite (admin_olift_installed_let_frame 0 1 h q), Hb.
 reflexivity.
Qed.

Lemma admin_krepl_frame_abort_hit (h : nat) (q : expr)
 (l : lctx) (e : expr) :
 joinable (admin_step)
 (krepl_e h (installed_let_frame h q)
 (ECont h (plug_l l (abort (ECont h e)))))
 (krepl_e h (installed_let_frame h q)
 (ECont h (plug_l l e))).
Proof.
 destruct (admin_krepl_installed_frame_tail_abort_shape h q l e)
 as [l' [ep [Hsrc Hdst]]].
 simpl. rewrite Nat.eqb_refl, Hsrc, Hdst.
 apply admin_abort_tail_spine.
Qed.

Lemma admin_krepl_abort_shape_nonhit (h : nat) (q : expr)
 (k : nat) (e : expr) :
 h <> k ->
 krepl_e h (installed_let_frame h q) (abort (ECont k e)) =
 abort (ECont k (krepl_e h (installed_let_frame h q) e)).
Proof.
 intro Hhk.
 assert (Hkh : Nat.eqb k h = false).
 { apply Nat.eqb_neq. intro Heq. apply Hhk. symmetry. exact Heq. }
 assert (Hskh : Nat.eqb (S k) (S h) = false).
 { apply Nat.eqb_neq. intro Heq. apply Hhk. lia. }
 assert (H0k : Nat.leb 0 k = true) by (apply Nat.leb_le; lia).
 assert (H0h : Nat.leb 0 h = true) by (apply Nat.leb_le; lia).
 assert (Hplus : Nat.eqb (k + 1) (S h) = false).
 { apply Nat.eqb_neq. intro Heq. apply Hhk. lia. }
 unfold abort. cbn [krepl_e]. cbn [klift_e].
 try rewrite H0k.
 try rewrite H0h.
 try rewrite Hplus.
 cbn [krepl_e].
 try rewrite H0h.
 try rewrite Hplus.
 f_equal.
 rewrite (admin_klift_krepl_e 0 h (installed_let_frame h q) e).
 reflexivity.
Qed.

Lemma admin_krepl_frame_tail_abort_shape_nonhit (h : nat) (q : expr)
 (k : nat) (l : lctx) (e : expr) :
 h <> k ->
 exists l' ep,
 krepl_e h (installed_let_frame h q)
 (plug_l l (abort (ECont k e))) =
 plug_l l' (abort (ECont k ep)) /\
 krepl_e h (installed_let_frame h q) (plug_l l e) = plug_l l' ep.
Proof.
 intro Hhk.
 revert q e.
 induction l as [|a l IH]; intros q e.
 - exists LNil, (krepl_e h (installed_let_frame h q) e). split.
 + apply admin_krepl_abort_shape_nonhit. exact Hhk.
 + reflexivity.
 - destruct (IH (olift_e 1 1 q) e)
 as [l' [ep [Ha Hb]]].
 exists (LLet (krepl_e h (installed_let_frame h q) a) l'), ep. split.
 + simpl.
 change (ELet (krepl_e h (installed_let_frame h q) a)
 (krepl_e h (olift_d 0 1 (installed_let_frame h q))
 (plug_l l (abort (ECont k e)))) =
 ELet (krepl_e h (installed_let_frame h q) a)
 (plug_l l' (abort (ECont k ep)))).
 rewrite (admin_olift_installed_let_frame 0 1 h q), Ha.
 reflexivity.
 + simpl.
 change (ELet (krepl_e h (installed_let_frame h q) a)
 (krepl_e h (olift_d 0 1 (installed_let_frame h q))
 (plug_l l e)) =
 ELet (krepl_e h (installed_let_frame h q) a) (plug_l l' ep)).
 rewrite (admin_olift_installed_let_frame 0 1 h q), Hb.
 reflexivity.
Qed.

Lemma admin_krepl_frame_abort_nonhit (h : nat) (q : expr)
 (k : nat) (l : lctx) (e : expr) :
 h <> k ->
 star (admin_step)
 (krepl_e h (installed_let_frame h q)
 (ECont k (plug_l l (abort (ECont k e)))))
 (krepl_e h (installed_let_frame h q)
 (ECont k (plug_l l e))).
Proof.
 intro Hhk.
 destruct (admin_krepl_frame_tail_abort_shape_nonhit h q k l e Hhk)
 as [l' [ep [Hsrc Hdst]]].
 assert (Hkh : Nat.eqb k h = false).
 { apply Nat.eqb_neq. intro Heq. apply Hhk. symmetry. exact Heq. }
 simpl. rewrite Hkh, Hsrc, Hdst.
 apply star_one. apply AS_ContTail.
 apply tail_step_plug_abort.
Qed.

Lemma admin_krepl_frame_abort_residual (h : nat) (q : expr)
 (k : nat) (l : lctx) (e : expr) :
 joinable (admin_step)
 (krepl_e h (installed_let_frame h q)
 (ECont k (plug_l l (abort (ECont k e)))))
 (krepl_e h (installed_let_frame h q)
 (ECont k (plug_l l e))).
Proof.
 destruct (Nat.eqb k h) eqn:Hkh.
 - apply Nat.eqb_eq in Hkh. subst k.
 apply admin_krepl_frame_abort_hit.
 - exists (krepl_e h (installed_let_frame h q)
 (ECont k (plug_l l e))); split.
 + apply admin_krepl_frame_abort_nonhit.
 intro Heq. subst k. rewrite Nat.eqb_refl in Hkh. discriminate.
 + apply star_refl.
Qed.

(**
 Naturality of the [Let.S] substitution.

 The continuation bound by the inner [EShift] is fresh for the ambient
 replacement. The statement below keeps those two binders separate: the
 ambient replacement is at [k], while the body is mapped at
 [S (k + cut)]. This is the equation needed when a [Let.S] root is
 transported through a continuation replacement.
 *)

Definition klift0_d (k : nat) (d : installed) : installed :=
 klift_d 0 k d.

Definition klift0_e (k : nat) (e : expr) : expr :=
 klift_e 0 k e.

Lemma admin_klift_add_d (a b : nat) (d : installed) :
 klift_d 0 a (klift_d 0 b d) = klift_d 0 (b + a) d.
Proof.
 destruct d as [j c]. simpl. f_equal.
 - destruct (Nat.leb 0 j); simpl; lia.
 - induction c as [|c IH tail]; simpl.
 + reflexivity.
 + rewrite IH. f_equal. apply fs_klift_comp_e.
Qed.

Lemma admin_klift_zero_d (cut : nat) (d : installed) :
 klift_d cut 0 d = d.
Proof.
 destruct d as [j c]. simpl. f_equal.
 - destruct (Nat.leb cut j); lia.
 - induction c as [|c IH tail]; simpl.
 + reflexivity.
 + rewrite IH, klift_zero_e. reflexivity.
Qed.

(* Removing a continuation binder from a continuation lifted above that
 binder is just the corresponding lift with the binder removed. This is
 the small arithmetic identity used by the non-hit dL.S fusion below. *)
Lemma admin_ksubst_lift_prefix (cut k : nat) (q : expr) :
 SharedPrompts.ksubst_e cut (ICont (k + cut) CHole)
 (klift_e 0 (S cut) q) = klift_e 0 cut q.
Proof.
 rewrite <- (SharedPrompts.MapComposition.klift_prefix_e 0 cut q).
 replace (0 + cut) with cut by lia.
 apply ksubst_klift_e.
Qed.

(* Non-hit dL.S fusion. The replacement head [h] and the dL.S delimiter
 [k] are distinct, so continuation removal commutes with the replacement;
 the shift raises both heads and the ordinary-let case raises the payload.
 This is an equality, rather than a reduction transport statement: it is
 the algebraic endpoint used by the corresponding residual gadget. *)
Lemma admin_ksubst_krepl_frame_nonhit :
 (forall v cut h k q,
 h <> k ->
 SharedPrompts.ksubst_v cut (ICont (k + cut) CHole)
 (krepl_v (S (h + cut))
 (klift_d 0 (S cut) (installed_let_frame h q)) v) =
 krepl_v (h + cut) (klift_d 0 cut (installed_let_frame h q))
 (SharedPrompts.ksubst_v cut (ICont (k + cut) CHole) v)) /\
 (forall e cut h k q,
 h <> k ->
 SharedPrompts.ksubst_e cut (ICont (k + cut) CHole)
 (krepl_e (S (h + cut))
 (klift_d 0 (S cut) (installed_let_frame h q)) e) =
 krepl_e (h + cut) (klift_d 0 cut (installed_let_frame h q))
 (SharedPrompts.ksubst_e cut (ICont (k + cut) CHole) e)).
Proof.
 apply (syntax_ind
 (fun v => forall cut h k q, h <> k ->
 SharedPrompts.ksubst_v cut (ICont (k + cut) CHole)
 (krepl_v (S (h + cut))
 (klift_d 0 (S cut) (installed_let_frame h q)) v) =
 krepl_v (h + cut) (klift_d 0 cut (installed_let_frame h q))
 (SharedPrompts.ksubst_v cut (ICont (k + cut) CHole) v))
 (fun e => forall cut h k q, h <> k ->
 SharedPrompts.ksubst_e cut (ICont (k + cut) CHole)
 (krepl_e (S (h + cut))
 (klift_d 0 (S cut) (installed_let_frame h q)) e) =
 krepl_e (h + cut) (klift_d 0 cut (installed_let_frame h q))
 (SharedPrompts.ksubst_e cut (ICont (k + cut) CHole) e))).
 - intros n cut h k q Hhk. reflexivity.
 - intros e IH cut h k q Hhk. simpl. f_equal.
 specialize (IH cut h k (olift_e 1 1 q) Hhk).
 simpl in IH.
 rewrite (klift_olift_e_comm 0 1 (S cut) 1 q) in IH.
 rewrite (klift_olift_e_comm 0 1 cut 1 q) in IH.
 exact IH.
 - intros v IH cut h k q Hhk. simpl. f_equal. apply IH; exact Hhk.
 - intros v IHv u IHu cut h k q Hhk. simpl. f_equal;
 [apply IHv | apply IHu]; exact Hhk.
 - intros a IHa t IHt cut h k q Hhk. simpl. f_equal.
 + apply IHa. exact Hhk.
 + specialize (IHt cut h k (olift_e 1 1 q) Hhk).
 simpl in IHt.
 rewrite (klift_olift_e_comm 0 1 (S cut) 1 q) in IHt.
 rewrite (klift_olift_e_comm 0 1 cut 1 q) in IHt.
 exact IHt.
 - intros e IH cut h k q Hhk. simpl. f_equal.
 specialize (IH (S cut) h k q Hhk).
 simpl in IH.
 assert (Hq1 : klift_e 0 1 (klift_e 0 (S cut) q) =
 klift_e 0 (S (S cut)) q).
 { rewrite (fs_klift_comp_e 0 1 (S cut) q).
 replace (S cut + 1) with (S (S cut)) by lia. reflexivity. }
 assert (Hq0 : klift_e 0 1 (klift_e 0 cut q) =
 klift_e 0 (S cut) q).
 { rewrite (fs_klift_comp_e 0 1 cut q).
 replace (cut + 1) with (S cut) by lia. reflexivity. }
 rewrite Hq1, Hq0.
 replace (S (S (h + cut))) with (S (h + S cut)) by lia.
 replace (h + S cut + 1) with (h + S (S cut)) by lia.
 replace (h + cut + 1) with (h + S cut) by lia.
 replace (k + cut + 1) with (k + S cut) by lia.
 replace (S (h + cut)) with (h + S cut) by lia.
 exact IH.
 - intros n e IH cut h k q Hhk. simpl.
 destruct (Nat.eqb n (S (h + cut))) eqn:Hnr.
 + apply Nat.eqb_eq in Hnr. subst n.
 replace (h + S cut) with (S (h + cut)) by lia.
 assert (Hremhit : remove_index cut (S (h + cut)) = Some (h + cut)).
 { apply remove_index_shift. lia. }
 cbn [SharedPrompts.ksubst_e]. rewrite Hremhit. simpl.
 assert (Hframe1 :
 ICont (S (h + cut)) (CLet CHole (klift_e 0 (S cut) q)) =
 klift_d 0 (S cut) (installed_let_frame h q)).
 { rewrite (admin_klift_installed_let_frame 0 (S cut) h q).
 unfold installed_let_frame. simpl.
 destruct (Nat.leb 0 h); f_equal; lia. }
 assert (Hframe0 :
 ICont (h + cut) (CLet CHole (klift_e 0 cut q)) =
 klift_d 0 cut (installed_let_frame h q)).
 { rewrite (admin_klift_installed_let_frame 0 cut h q).
 unfold installed_let_frame. simpl.
 destruct (Nat.leb 0 h); f_equal; lia. }
 rewrite Hframe1, Hframe0.
 rewrite Nat.eqb_refl. f_equal. f_equal.
 * rewrite (IH cut h k q Hhk). reflexivity.
 * apply admin_ksubst_lift_prefix.
 + destruct (remove_index cut n) as [j|] eqn:Hrem.
 * cbn [SharedPrompts.ksubst_e]. rewrite Hrem. simpl.
 replace (h + S cut) with (S (h + cut)) by lia.
 assert (Hnc : Nat.eqb n cut = false).
 { unfold remove_index in Hrem.
 destruct (Nat.eqb n cut); discriminate || reflexivity. }
 assert (Hj : Nat.eqb j (h + cut) = false).
 { pose proof (@remove_index_eqb_above cut n (h + cut)
 ltac:(lia) Hnc) as Hmap.
 rewrite Hrem in Hmap. simpl in Hmap.
 rewrite Hnr in Hmap. exact Hmap. }
 assert (Hframe1 :
 ICont (S (h + cut)) (CLet CHole (klift_e 0 (S cut) q)) =
 klift_d 0 (S cut) (installed_let_frame h q)).
 { rewrite (admin_klift_installed_let_frame 0 (S cut) h q).
 unfold installed_let_frame. simpl.
 destruct (Nat.leb 0 h); f_equal; lia. }
 assert (Hframe0 :
 ICont (h + cut) (CLet CHole (klift_e 0 cut q)) =
 klift_d 0 cut (installed_let_frame h q)).
 { rewrite (admin_klift_installed_let_frame 0 cut h q).
 unfold installed_let_frame. simpl.
 destruct (Nat.leb 0 h); f_equal; lia. }
 rewrite Hframe1, Hframe0, Hj. f_equal.
 apply IH. exact Hhk.
 * cbn [SharedPrompts.ksubst_e]. rewrite Hrem. simpl.
 replace (h + S cut) with (S (h + cut)) by lia.
 assert (Hkh : Nat.eqb (k + cut) (h + cut) = false).
 { apply Nat.eqb_neq. intro Heq. apply Hhk. lia. }
 assert (Hframe1 :
 ICont (S (h + cut)) (CLet CHole (klift_e 0 (S cut) q)) =
 klift_d 0 (S cut) (installed_let_frame h q)).
 { rewrite (admin_klift_installed_let_frame 0 (S cut) h q).
 unfold installed_let_frame. simpl.
 destruct (Nat.leb 0 h); f_equal; lia. }
 assert (Hframe0 :
 ICont (h + cut) (CLet CHole (klift_e 0 cut q)) =
 klift_d 0 cut (installed_let_frame h q)).
 { rewrite (admin_klift_installed_let_frame 0 cut h q).
 unfold installed_let_frame. simpl.
 destruct (Nat.leb 0 h); f_equal; lia. }
 rewrite Hframe1, Hframe0, Hkh. f_equal.
 apply IH. exact Hhk.
 - intros n cut h k q Hhk. simpl.
 destruct (Nat.eqb n (S (h + cut))) eqn:Hnr.
 + apply Nat.eqb_eq in Hnr. subst n.
 cbn [SharedPrompts.ksubst_e].
 replace (h + S cut) with (S (h + cut)) by lia.
 assert (Hremhit : remove_index cut (S (h + cut)) = Some (h + cut)).
 { apply remove_index_shift. lia. }
 rewrite Hremhit.
 simpl. rewrite Nat.eqb_refl. reflexivity.
 + destruct (remove_index cut n) as [j|] eqn:Hrem.
 * cbn [SharedPrompts.ksubst_e]. rewrite Hrem. simpl.
 assert (Hnc : Nat.eqb n cut = false).
 { unfold remove_index in Hrem.
 destruct (Nat.eqb n cut); discriminate || reflexivity. }
 assert (Hj : Nat.eqb j (h + cut) = false).
 { pose proof (@remove_index_eqb_above cut n (h + cut)
 ltac:(lia) Hnc) as Hmap.
 rewrite Hrem in Hmap. simpl in Hmap.
 rewrite Hnr in Hmap. exact Hmap. }
 rewrite Hj. reflexivity.
 * cbn [SharedPrompts.ksubst_e]. rewrite Hrem. simpl.
 assert (Hkh : Nat.eqb (k + cut) (h + cut) = false).
 { apply Nat.eqb_neq. intro Heq. apply Hhk. lia. }
 rewrite Hkh. reflexivity.
Qed.

(* With a non-hit outer frame, the dL.S residual is now a direct instance of
 the fusion equation above. The tail induction only lifts the same
 joinability through ordinary let frames. *)
Lemma admin_krepl_frame_tail_shift_nonhit_tail (h : nat) (q : expr)
 (k : nat) (l : lctx) (e : expr) :
 h <> k -> cocc_e 0 e = true ->
 joinable (delimited_step k)
 (krepl_e h (installed_let_frame h q) (plug_l l (EShift e)))
 (krepl_e h (installed_let_frame h q)
 (plug_l l (abort (SharedPrompts.ksubst_e 0 (ICont k CHole) e)))).
Proof.
 intros Hhk Hocc.
 revert q e Hocc.
 induction l as [|a l IH]; intros q e Hocc.
 - assert (Hocc_m :
 cocc_e 0
 (krepl_e (S h) (klift_d 0 1 (installed_let_frame h q)) e) = true).
 { rewrite (admin_klift_installed_let_frame 0 1 h q).
 destruct (Nat.leb 0 h) eqn:Hh; simpl.
 - replace (h + 1) with (S h) by lia.
 apply (proj2 admin_cocc_krepl_installed_frame e 0 (S h)
 (klift_e 0 1 q)); [lia | exact Hocc].
 - exfalso. apply Nat.leb_gt in Hh. lia. }
 assert (Hfus := (proj2 admin_ksubst_krepl_frame_nonhit
 e 0 h k q Hhk)).
 assert (Hlift := admin_klift_krepl_e 0 h (installed_let_frame h q)
 (SharedPrompts.ksubst_e 0 (ICont k CHole) e)).
 idtac.
 idtac.
 simpl.
 assert (Hframe1 :
 ICont (h + 1) (CLet CHole (klift_e 0 1 q)) =
 klift_d 0 1 (installed_let_frame h q)).
 { rewrite (admin_klift_installed_let_frame 0 1 h q).
 destruct (Nat.leb 0 h) eqn:Hh; simpl.
 - unfold installed_let_frame. reflexivity.
 - exfalso. apply Nat.leb_gt in Hh. lia. }
 rewrite Hframe1.
 replace (k + 0) with k in Hfus by lia.
 replace (h + 0) with h in Hfus by lia.
 replace (S (h + 0)) with (S h) in Hfus by lia.
 rewrite (admin_klift_zero_d 0 (installed_let_frame h q)) in Hfus.
 exists (abort (SharedPrompts.ksubst_e 0 (ICont k CHole)
 (krepl_e (S h) (klift_d 0 1 (installed_let_frame h q)) e))).
 split.
 + apply star_one. right. apply TS_Shift. exact Hocc_m.
 + unfold abort. simpl.
 rewrite Hframe1.
 rewrite Hfus.
 rewrite Hlift.
 destruct (Nat.leb 0 h) eqn:Hh; simpl.
 * apply star_refl.
 * exfalso. apply Nat.leb_gt in Hh. lia.
 - simpl.
 assert (Hframe :
 ICont h (CLet CHole (olift_e 1 1 q)) =
 installed_let_frame h (olift_e 1 1 q)) by reflexivity.
 rewrite Hframe.
 apply (admin_joinable_map (delimited_step k) (delimited_step k)
 (ELet (krepl_e h (installed_let_frame h q) a))).
 + intros x y Hxy. apply admin_tail_step_let_r. exact Hxy.
 + apply IH. exact Hocc.
Qed.

Lemma admin_krepl_frame_tail_shift_nonhit (h : nat) (q : expr)
 (k : nat) (l : lctx) (e : expr) :
 h <> k -> cocc_e 0 e = true ->
 joinable (admin_step)
 (krepl_e h (installed_let_frame h q)
 (ECont k (plug_l l (EShift e))))
 (krepl_e h (installed_let_frame h q)
 (ECont k (plug_l l
 (abort (SharedPrompts.ksubst_e 0 (ICont k CHole) e))))).
Proof.
 intros Hhk Hocc.
 assert (Hbody := admin_krepl_frame_tail_shift_nonhit_tail h q k l e
 Hhk Hocc).
 destruct Hbody as [w [Hw1 Hw2]].
 simpl.
 assert (Hkh : Nat.eqb k h = false).
 { apply Nat.eqb_neq. intro Heq. apply Hhk. symmetry. exact Heq. }
 rewrite Hkh.
 exists (ECont k w); split.
 - apply admin_tail_star_lift. exact Hw1.
 - apply admin_tail_star_lift. exact Hw2.
Qed.

(* The complete dL.S frame transport, isolating only the genuine hit case
 as a premise. The non-hit branch is the fusion lemma above; AbortD is
 already handled by the explicit abort/spine residual. *)
Lemma admin_frame_tail_compatibility_from_shift_hit
 (Hshift : forall h q l e,
 cocc_e 0 e = true ->
 joinable (admin_step)
 (krepl_e h (installed_let_frame h q)
 (ECont h (plug_l l (EShift e))))
 (krepl_e h (installed_let_frame h q)
 (ECont h (plug_l l
 (abort (SharedPrompts.ksubst_e 0 (ICont h CHole) e)))))) :
 forall h q k e e',
 tail_step k e e' ->
 joinable (admin_step)
 (krepl_e h (installed_let_frame h q) (ECont k e))
 (krepl_e h (installed_let_frame h q) (ECont k e')).
Proof.
 intros h q k e e' Hd.
 pose proof (tail_step_shape k e e' Hd) as Hshape.
 destruct Hshape as [Hshape|Hshape].
 - destruct Hshape as [l [r [Hsrc [Hdst Hocc]]]].
 rewrite Hsrc, Hdst.
 destruct (Nat.eqb k h) eqn:Hkh.
 + apply Nat.eqb_eq in Hkh. subst k. apply Hshift. exact Hocc.
 + apply admin_krepl_frame_tail_shift_nonhit; [|exact Hocc].
 intro Heq. subst k. rewrite Nat.eqb_refl in Hkh. discriminate.
 - destruct Hshape as [l [r [Hsrc Hdst]]].
 rewrite Hsrc, Hdst. apply admin_krepl_frame_abort_residual.
Qed.

(* A continuation replacement at [k+b] cannot hit an occurrence lifted by
 [b] above the fresh continuation [k]. *)
Lemma admin_krepl_klift_nohit :
 (forall v b k f,
 krepl_v (k + b) f (klift_v b (S k) v) =
 klift_v b (S k) v) /\
 (forall e b k f,
 krepl_e (k + b) f (klift_e b (S k) e) =
 klift_e b (S k) e).
Proof.
 apply (syntax_ind
 (fun v => forall b k f,
 krepl_v (k + b) f (klift_v b (S k) v) =
 klift_v b (S k) v)
 (fun e => forall b k f,
 krepl_e (k + b) f (klift_e b (S k) e) =
 klift_e b (S k) e)).
 - intros n b k f. reflexivity.
 - intros e IH b k f. simpl. f_equal.
 rewrite (IH b k (olift_d 0 1 f)). reflexivity.
 - intros v IH b k f. simpl. f_equal. apply IH.
 - intros v IHv u IHu b k f. simpl. f_equal; [apply IHv|apply IHu].
 - intros a IHa t IHt b k f. simpl. f_equal.
 + apply IHa.
 + apply IHt.
 - intros e IH b k f. simpl. f_equal.
 replace (S (k + b)) with (k + S b) by lia.
 apply IH.
 - intros n e IH b k f. simpl.
 destruct (Nat.leb b n) eqn:Hbn; simpl.
 + replace (k + b + (S k)) with (S k + (k + b)) by lia.
 apply Nat.leb_le in Hbn.
 assert (Hneq : Nat.eqb (n + S k) (k + b) = false).
 { apply Nat.eqb_neq. lia. }
 rewrite Hneq. f_equal. apply IH.
 + assert (Hbn' : n < b) by (apply Nat.leb_gt; exact Hbn).
 assert (Hneq : Nat.eqb n (k + b) = false).
 { apply Nat.eqb_neq. lia. }
 rewrite Hneq. f_equal. apply IH.
 - intros n b k f. simpl.
 destruct (Nat.leb b n) eqn:Hbn; simpl.
 + replace (k + b + (S k)) with (S k + (k + b)) by lia.
 apply Nat.leb_le in Hbn.
 assert (Hneq : Nat.eqb (n + S k) (k + b) = false).
 { apply Nat.eqb_neq. lia. }
 rewrite Hneq. reflexivity.
 + assert (Hbn' : n < b) by (apply Nat.leb_gt; exact Hbn).
 assert (Hneq : Nat.eqb n (k + b) = false).
 { apply Nat.eqb_neq. lia. }
 rewrite Hneq. reflexivity.
Qed.

(* Hit-case fusion for the two replacements generated by a Let.S residual.
 The outer continuation removal meets the fresh frame head exactly at
 [h+cut]; the equation is the algebraic core of the frame-hit gadget. *)
Lemma admin_ksubst_krepl_frame_hit :
 (forall v cut h q,
 SharedPrompts.ksubst_v cut (ICont (h + cut) CHole)
 (krepl_v cut (installed_let_frame cut (klift_e 0 (S cut) q))
 (krepl_v (S (h + cut))
 (klift_d 0 (S cut) (installed_let_frame h q)) v)) =
 krepl_v (h + cut) (klift_d 0 cut (installed_let_frame h q))
 (SharedPrompts.ksubst_v cut (ICont (h + cut) CHole) v)) /\
 (forall e cut h q,
 SharedPrompts.ksubst_e cut (ICont (h + cut) CHole)
 (krepl_e cut (installed_let_frame cut (klift_e 0 (S cut) q))
 (krepl_e (S (h + cut))
 (klift_d 0 (S cut) (installed_let_frame h q)) e)) =
 krepl_e (h + cut) (klift_d 0 cut (installed_let_frame h q))
 (SharedPrompts.ksubst_e cut (ICont (h + cut) CHole) e)).
Proof.
 apply (syntax_ind
 (fun v => forall cut h q,
 SharedPrompts.ksubst_v cut (ICont (h + cut) CHole)
 (krepl_v cut (installed_let_frame cut (klift_e 0 (S cut) q))
 (krepl_v (S (h + cut))
 (klift_d 0 (S cut) (installed_let_frame h q)) v)) =
 krepl_v (h + cut) (klift_d 0 cut (installed_let_frame h q))
 (SharedPrompts.ksubst_v cut (ICont (h + cut) CHole) v))
 (fun e => forall cut h q,
 SharedPrompts.ksubst_e cut (ICont (h + cut) CHole)
 (krepl_e cut (installed_let_frame cut (klift_e 0 (S cut) q))
 (krepl_e (S (h + cut))
 (klift_d 0 (S cut) (installed_let_frame h q)) e)) =
 krepl_e (h + cut) (klift_d 0 cut (installed_let_frame h q))
 (SharedPrompts.ksubst_e cut (ICont (h + cut) CHole) e))).
 - intros n cut h q. reflexivity.
 - intros e IH cut h q. simpl. f_equal.
 specialize (IH cut h (olift_e 1 1 q)).
 simpl in IH.
 rewrite (klift_olift_e_comm 0 1 (S cut) 1 q) in IH.
 rewrite (klift_olift_e_comm 0 1 cut 1 q) in IH.
 exact IH.
 - intros v IH cut h q. simpl. f_equal. apply IH.
 - intros v IHv u IHu cut h q. simpl. f_equal;
 [apply IHv | apply IHu].
 - intros a IHa t IHt cut h q. simpl. f_equal.
 + apply IHa.
 + specialize (IHt cut h (olift_e 1 1 q)).
 simpl in IHt.
 rewrite (klift_olift_e_comm 0 1 (S cut) 1 q) in IHt.
 rewrite (klift_olift_e_comm 0 1 cut 1 q) in IHt.
 exact IHt.
 - intros e IH cut h q. simpl. f_equal.
 specialize (IH (S cut) h q).
 simpl in IH.
 replace (h + cut + 1) with (h + S cut) by lia.
 replace (cut + 1) with (S cut) by lia.
 replace (S (S (h + cut))) with (S (h + S cut)) by lia.
 replace (h + S cut + 1) with (h + S (S cut)) by lia.
 replace (h + cut + 1) with (h + S cut) by lia.
 rewrite (fs_klift_comp_e 0 1 (S cut) q).
 rewrite (fs_klift_comp_e 0 1 cut q).
 replace (S cut + 1) with (S (S cut)) by lia.
 replace (cut + 1) with (S cut) by lia.
 unfold installed_let_frame in IH |- *.
 replace (S (h + cut)) with (h + S cut) by lia.
 exact IH.
 - intros n e IH cut h q. simpl.
 destruct (Nat.eqb n (S (h + cut))) eqn:Hinner.
 + destruct (Nat.eqb n (h + cut)) eqn:Houter; simpl.
 * apply Nat.eqb_eq in Hinner.
 apply Nat.eqb_eq in Houter. lia.
 * apply Nat.eqb_eq in Hinner. subst n.
 assert (Hneq : Nat.eqb (S (h + cut)) cut = false) by
 (apply Nat.eqb_neq; lia).
 assert (Hneq2 : Nat.eqb (h + S cut) cut = false) by
 (apply Nat.eqb_neq; lia).
 rewrite Hneq2.
 cbn [SharedPrompts.ksubst_e].
 cbn [SharedPrompts.krepl_e].
 cbn [SharedPrompts.remove_index].
 assert (Hrem : remove_index cut (h + S cut) = Some (h + cut)).
 { replace (h + S cut) with (S (h + cut)) by lia.
 apply remove_index_shift. lia. }
 rewrite Hrem.
 assert (Hrem2 : remove_index cut (S (h + cut)) = Some (h + cut)).
 { apply remove_index_shift. lia. }
 rewrite Hrem2.
 cbn [SharedPrompts.krepl_e].
 rewrite Nat.eqb_refl.
 cbn [plug_d].
 unfold plug, installed_let_frame. simpl.
 assert (Hframe0 :
 ICont (h + cut) (CLet CHole (klift_e 0 cut q)) =
 klift_d 0 cut (installed_let_frame h q)).
 { rewrite (admin_klift_installed_let_frame 0 cut h q).
 unfold installed_let_frame. simpl.
 destruct (Nat.leb 0 h); f_equal; lia. }
 assert (Hframe1 :
 ICont (h + S cut) (CLet CHole (klift_e 0 (S cut) q)) =
 klift_d 0 (S cut) (installed_let_frame h q)).
 { rewrite (admin_klift_installed_let_frame 0 (S cut) h q).
 unfold installed_let_frame. simpl.
 destruct (Nat.leb 0 h); f_equal; lia. }
 f_equal.
 f_equal.
 { rewrite Hframe1.
 unfold installed_let_frame in IH |- *.
 rewrite IH. rewrite Hframe0. reflexivity. }
 { pose proof (proj2 admin_krepl_klift_nohit q 0 cut
 (ICont cut (CLet CHole (olift_e 1 1 (klift_e 0 (S cut) q)))))
 as Hno.
 replace (cut + 0) with cut in Hno by lia.
 rewrite Hno.
 apply admin_ksubst_lift_prefix. }
 + destruct (Nat.eqb n (h + cut)) eqn:Houter; simpl.
 * apply Nat.eqb_eq in Houter. subst n.
 destruct h as [|h].
 (* The outer hit is also the cut-zero case. *)
 { rewrite Nat.eqb_refl.
 cbn [SharedPrompts.ksubst_e].
 rewrite remove_index_eq. simpl.
 cbn [SharedPrompts.krepl_e].
 cbn [plug_d].
 rewrite remove_index_eq. simpl.
 cbn [SharedPrompts.krepl_e].
 cbn [plug_d].
 rewrite Nat.eqb_refl.
 assert (Hframe1 :
 ICont (S cut) (CLet CHole (klift_e 0 (S cut) q)) =
 klift_d 0 (S cut) (installed_let_frame 0 q)).
 { rewrite (admin_klift_installed_let_frame 0 (S cut) 0 q).
 unfold installed_let_frame. simpl. reflexivity. }
 f_equal. f_equal.
 { rewrite Hframe1.
 replace (0 + cut) with cut by lia.
 replace (S (0 + cut)) with (S cut) by lia.
 exact (IH cut 0 q). }
 { exact (admin_ksubst_lift_prefix cut 0 q). } }
 (* For a positive offset, removal decrements the head and neither
 replacement hits it. *)
 { assert (Hneq : Nat.eqb (S h + cut) (S (S h + cut)) = false) by
 (apply Nat.eqb_neq; lia).
 assert (Hneq2 : Nat.eqb (S h + cut) cut = false) by
 (apply Nat.eqb_neq; lia).
 rewrite Hneq2.
 assert (Hrem : remove_index cut (S h + cut) = Some (h + cut)).
 { replace (S h + cut) with (S (h + cut)) by lia.
 apply remove_index_shift. lia. }
 cbn [SharedPrompts.ksubst_e]. rewrite Hrem. simpl.
 assert (Hhead : Nat.eqb (h + cut) (S h + cut) = false) by
 (apply Nat.eqb_neq; lia).
 assert (Hhead2 : Nat.eqb (h + cut) (S (h + cut)) = false) by
 (apply Nat.eqb_neq; lia).
 rewrite Hhead2.
 cbn [SharedPrompts.krepl_e].
 f_equal.
 replace (S (h + cut)) with (S h + cut) by lia.
 replace (S (S (h + cut))) with (S (S h + cut)) by lia.
 replace (S (h + S cut)) with (S (S h + cut)) by lia.
 assert (Hframe1 :
 ICont (S (S h + cut))
 (CLet CHole (klift_e 0 (S cut) q)) =
 klift_d 0 (S cut) (installed_let_frame (S h) q)).
 { rewrite (admin_klift_installed_let_frame 0 (S cut) (S h) q).
 unfold installed_let_frame. simpl.
 destruct (Nat.leb 0 (S h)); f_equal; lia. }
 assert (Hframe0 :
 ICont (S h + cut) (CLet CHole (klift_e 0 cut q)) =
 klift_d 0 cut (installed_let_frame (S h) q)).
 { rewrite (admin_klift_installed_let_frame 0 cut (S h) q).
 unfold installed_let_frame. simpl.
 destruct (Nat.leb 0 (S h)); f_equal; lia. }
 rewrite Hframe1, Hframe0.
 exact (IH cut (S h) q).
 }
 * destruct (Nat.eqb n cut) eqn:Hcut; simpl.
 { apply Nat.eqb_eq in Hcut. subst n.
 rewrite remove_index_eq. simpl.
 cbn [SharedPrompts.krepl_e].
 rewrite Nat.eqb_refl.
 cbn [plug_d].
 assert (Hframe1 :
 ICont (h + S cut) (CLet CHole (klift_e 0 (S cut) q)) =
 klift_d 0 (S cut) (installed_let_frame h q)).
 { rewrite (admin_klift_installed_let_frame 0 (S cut) h q).
 unfold installed_let_frame. simpl.
 destruct (Nat.leb 0 h); f_equal; lia. }
 assert (Hframe0 :
 ICont (h + cut) (CLet CHole (klift_e 0 cut q)) =
 klift_d 0 cut (installed_let_frame h q)).
 { rewrite (admin_klift_installed_let_frame 0 cut h q).
 unfold installed_let_frame. simpl.
 destruct (Nat.leb 0 h); f_equal; lia. }
 f_equal. f_equal.
 { rewrite Hframe1. rewrite (IH cut h q). rewrite Hframe0. reflexivity. }
 { exact (admin_ksubst_lift_prefix cut h q). } }
 { destruct (remove_index cut n) as [j|] eqn:Hrem.
 - cbn [SharedPrompts.ksubst_e]. simpl.
 assert (Hnc : Nat.eqb n cut = false). exact Hcut.
 assert (Hj : Nat.eqb j (h + cut) = false).
 { pose proof (@remove_index_eqb_above cut n (h + cut)
 ltac:(lia) Hnc) as Hmap.
 rewrite Hrem in Hmap. simpl in Hmap.
 rewrite Hinner in Hmap. exact Hmap. }
 rewrite Hj.
 cbn [SharedPrompts.krepl_e].
 f_equal.
 assert (Hframe1 :
 ICont (h + S cut) (CLet CHole (klift_e 0 (S cut) q)) =
 klift_d 0 (S cut) (installed_let_frame h q)).
 { rewrite (admin_klift_installed_let_frame 0 (S cut) h q).
 unfold installed_let_frame. simpl.
 destruct (Nat.leb 0 h); f_equal; lia. }
 rewrite Hframe1.
 assert (Hframe0 :
 ICont (h + cut) (CLet CHole (klift_e 0 cut q)) =
 klift_d 0 cut (installed_let_frame h q)).
 { rewrite (admin_klift_installed_let_frame 0 cut h q).
 unfold installed_let_frame. simpl.
 destruct (Nat.leb 0 h); f_equal; lia. }
 rewrite Hframe0.
 exact (IH cut h q).
 - exfalso.
 unfold remove_index in Hrem.
 rewrite Hcut in Hrem.
 destruct (Nat.leb (S cut) n); discriminate. }
 - intros n cut h q. simpl.
 destruct (Nat.eqb n (S (h + cut))) eqn:Hinner.
 + destruct (Nat.eqb n (h + cut)) eqn:Houter.
 * apply Nat.eqb_eq in Hinner.
 apply Nat.eqb_eq in Houter. lia.
 * destruct (remove_index cut n) as [j|] eqn:Hrem; simpl.
 { apply Nat.eqb_eq in Hinner. subst n.
 assert (Hneq : Nat.eqb (h + S cut) cut = false) by
 (apply Nat.eqb_neq; lia).
 rewrite Hneq.
 cbn [SharedPrompts.ksubst_e].
 assert (Hrem2 : remove_index cut (h + S cut) = Some (h + cut)).
 { replace (h + S cut) with (S (h + cut)) by lia.
 apply remove_index_shift. lia. }
 rewrite Hrem2.
 assert (Hnc : Nat.eqb (S (h + cut)) cut = false).
 { unfold remove_index in Hrem.
 destruct (Nat.eqb (S (h + cut)) cut); discriminate || reflexivity. }
 assert (Hmap : Nat.eqb j (h + cut) = true).
 { pose proof (@remove_index_eqb_above cut (S (h + cut)) (h + cut)
 ltac:(lia) Hnc) as H0.
 rewrite Hrem in H0. simpl in H0.
 destruct (Nat.eqb (h + cut) (h + cut)) eqn:Hself in H0;
 simpl in H0.
 - exact H0.
 - rewrite Nat.eqb_refl in Hself. discriminate. }
 rewrite Hmap.
 cbn [SharedPrompts.ksubst_e].
 reflexivity. }
 { apply Nat.eqb_eq in Hinner. subst n.
 assert (Hneq : Nat.eqb (h + S cut) cut = false) by
 (apply Nat.eqb_neq; lia).
 rewrite Hneq.
 assert (Hrem2 : remove_index cut (h + S cut) = Some (h + cut)).
 { replace (h + S cut) with (S (h + cut)) by lia.
 apply remove_index_shift. lia. }
 cbn [SharedPrompts.ksubst_e]. rewrite Hrem2.
 rewrite Nat.eqb_refl. reflexivity. }
 + destruct (Nat.eqb n (h + cut)) eqn:Houter.
 * destruct (remove_index cut n) as [j|] eqn:Hrem; simpl.
 { apply Nat.eqb_eq in Houter. subst n.
 assert (Hnc : Nat.eqb (h + cut) cut = false).
 { unfold remove_index in Hrem.
 destruct (Nat.eqb (h + cut) cut); discriminate || reflexivity. }
 cbn [SharedPrompts.ksubst_e].
 rewrite Hnc.
 cbn [remove_index].
 assert (Hmap : Nat.eqb j (h + cut) = false).
 { pose proof (@remove_index_eqb_above cut (h + cut) (h + cut)
 ltac:(lia) Hnc) as H0.
 rewrite Hrem in H0. simpl in H0.
 rewrite Hinner in H0. exact H0. }
 rewrite Hmap.
 cbn [SharedPrompts.ksubst_e].
 rewrite Hrem. reflexivity. }
 { apply Nat.eqb_eq in Houter. subst n.
 destruct h as [|h].
 - cbn [SharedPrompts.ksubst_e].
 replace (0 + cut) with cut by lia.
 rewrite Nat.eqb_refl. simpl.
 rewrite remove_index_eq. reflexivity.
 - exfalso.
 unfold remove_index in Hrem.
 assert (Hneq : Nat.eqb (S h + cut) cut = false) by
 (apply Nat.eqb_neq; lia).
 rewrite Hneq in Hrem.
 destruct (Nat.leb (S cut) (S h + cut)); discriminate. }
 * destruct (remove_index cut n) as [j|] eqn:Hrem; simpl.
 { cbn [SharedPrompts.ksubst_e].
 assert (Hnc : Nat.eqb n cut = false).
 { unfold remove_index in Hrem.
 destruct (Nat.eqb n cut); discriminate || reflexivity. }
 assert (Hmap : Nat.eqb j (h + cut) = false).
 { pose proof (@remove_index_eqb_above cut n (h + cut)
 ltac:(lia) Hnc) as H0.
 rewrite Hrem in H0. simpl in H0.
 rewrite Hinner in H0. exact H0. }
 rewrite Hmap.
 rewrite Hnc.
 cbn [SharedPrompts.ksubst_e].
 rewrite Hrem. reflexivity. }
 { destruct (Nat.eqb n cut) eqn:Hcut; simpl.
 - apply Nat.eqb_eq in Hcut. subst n.
 cbn [SharedPrompts.ksubst_e].
 rewrite Nat.eqb_refl.
 rewrite remove_index_eq. reflexivity.
 - cbn [SharedPrompts.ksubst_e].
 rewrite Hrem. simpl. rewrite Nat.eqb_refl. reflexivity. }
Qed.

(* Empty-tail hit residual. The mapped source first exposes a Let.S redex;
 the resulting tail shift is then contracted by dL.S. On the target the
 same Let.S step is a stutter after [krepl] meets the freshly lifted body.
 The two endpoints are identified by [admin_ksubst_krepl_frame_hit]. *)
Lemma admin_krepl_frame_tail_shift_hit_empty (h : nat) (q e : expr) :
 cocc_e 0 e = true ->
 joinable (admin_step)
 (krepl_e h (installed_let_frame h q) (ECont h (EShift e)))
 (krepl_e h (installed_let_frame h q)
 (ECont h (abort (SharedPrompts.ksubst_e 0 (ICont h CHole) e)))).
Proof.
 intro Hocc.
 set (R := krepl_e (S h) (klift_d 0 1 (installed_let_frame h q)) e).
 set (T := krepl_e h (installed_let_frame h q)
 (SharedPrompts.ksubst_e 0 (ICont h CHole) e)).
 assert (Hfus :
 SharedPrompts.ksubst_e 0 (ICont h CHole)
 (krepl_e 0 (frame q) R) = T).
 { unfold R, T.
 rewrite (admin_frame_eq q).
 replace (0 + h) with h by lia.
 replace (S (h + 0)) with (S h) by lia.
 pose proof (proj2 admin_ksubst_krepl_frame_hit e 0 h q) as H.
 replace (h + 0) with h in H by lia.
 replace (S (h + 0)) with (S h) in H by lia.
 rewrite (admin_klift_zero_d 0 (installed_let_frame h q)) in H.
 exact H. }
 assert (HoccR : cocc_e 0 (krepl_e 0 (frame q) R) = true).
 { unfold R.
 rewrite (admin_frame_eq q).
 apply (proj2 admin_cocc_krepl_installed_frame
 (krepl_e (S h) (klift_d 0 1 (installed_let_frame h q)) e)
 0 0 (klift_e 0 1 q)); [lia |].
 rewrite (admin_klift_installed_let_frame 0 1 h q).
 destruct (Nat.leb 0 h) eqn:Hh; simpl.
 - replace (h + 1) with (S h) by lia.
 apply (proj2 admin_cocc_krepl_installed_frame e 0 (S h)
 (klift_e 0 1 q)); [lia | exact Hocc].
 - exfalso. apply Nat.leb_gt in Hh. lia. }
 assert (Hsrc :
 krepl_e h (installed_let_frame h q) (ECont h (EShift e)) =
 ECont h (ELet (EShift R) q)).
 { unfold R.
 simpl. rewrite Nat.eqb_refl.
 simpl.
 replace (h + 1) with (S h) by lia.
 destruct (Nat.leb 0 h) eqn:Hh; simpl.
 - reflexivity.
 - exfalso. apply Nat.leb_gt in Hh. lia. }
 assert (Hdst :
 krepl_e h (installed_let_frame h q)
 (ECont h (abort (SharedPrompts.ksubst_e 0 (ICont h CHole) e))) =
 ECont h (ELet (abort T) q)).
 { unfold T.
 simpl. rewrite Nat.eqb_refl.
 simpl.
 replace (h + 1) with (S h) by lia.
 destruct (Nat.leb 0 h) eqn:Hh; simpl.
 - assert (Hframe1 :
 ICont (S h) (CLet CHole (klift_e 0 1 q)) =
 klift_d 0 1 (installed_let_frame h q)).
 { rewrite (admin_klift_installed_let_frame 0 1 h q).
 unfold installed_let_frame. simpl.
 replace (h + 1) with (S h) by lia.
 reflexivity. }
 rewrite Hframe1.
 pose proof (admin_klift_krepl_e 0 h (installed_let_frame h q)
 (SharedPrompts.ksubst_e 0 (ICont h CHole) e)) as Hlift.
 rewrite Hh in Hlift.
 rewrite <- Hlift.
 reflexivity.
 - exfalso. apply Nat.leb_gt in Hh. lia. }
 rewrite Hsrc, Hdst.
 exists (ECont h (abort T)); split.
 - eapply star_trans.
 + apply star_one. apply AS_ContBody. apply AS_LetShift.
 + eapply star_trans.
 * apply star_one. apply AS_ContTail. apply TS_Shift.
 exact HoccR.
 * rewrite Hfus. apply star_refl.
 - assert (Hfix := admin_krepl_klift_fixed 0 (frame q) T).
 unfold abort.
 eapply star_trans.
 + apply star_one. apply AS_ContBody. apply AS_LetShift.
 + rewrite Hfix. apply star_refl.
Qed.

(* A nonempty tail contributes the same outer LetLet step on both mapped
 arms. After that reassociation, the shorter-tail residual sits under one
 additional right-let frame of the same continuation mode. *)
Lemma admin_krepl_frame_tail_shift_hit (h : nat) (q : expr)
 (l : lctx) (e : expr) :
 cocc_e 0 e = true ->
 joinable (admin_step)
 (krepl_e h (installed_let_frame h q)
 (ECont h (plug_l l (EShift e))))
 (krepl_e h (installed_let_frame h q)
 (ECont h (plug_l l
 (abort (SharedPrompts.ksubst_e 0 (ICont h CHole) e))))).
Proof.
 intro Hocc. revert q.
 induction l as [|a l IH]; intro q.
 - apply admin_krepl_frame_tail_shift_hit_empty. exact Hocc.
 - set (q' := olift_e 1 1 q).
 set (a' := krepl_e h (installed_let_frame h q) a).
 set (s := krepl_e h (installed_let_frame h q') (plug_l l (EShift e))).
 set (t := krepl_e h (installed_let_frame h q')
 (plug_l l
 (abort (SharedPrompts.ksubst_e 0 (ICont h CHole) e)))).
 assert (HIH : joinable (admin_step)
 (ECont h (ELet s q'))
 (ECont h (ELet t q'))).
 { pose proof (IH q') as H.
 unfold s, t.
 cbn [krepl_e] in H.
 rewrite Nat.eqb_refl in H.
 exact H. }
 pose proof (admin_joinable_cont_let_r h a'
 (ELet s q') (ELet t q') HIH) as Hjoin.
 destruct Hjoin as [w [Hs Ht]].
 exists w. split.
 + eapply star_step.
 * unfold a', s, q'.
 cbn [plug_l krepl_e]. rewrite Nat.eqb_refl.
 rewrite (admin_olift_installed_let_frame 0 1 h q).
 apply AS_ContBody. apply AS_LetAssoc.
 * exact Hs.
 + eapply star_step.
 * unfold a', t, q'.
 cbn [plug_l krepl_e]. rewrite Nat.eqb_refl.
 rewrite (admin_olift_installed_let_frame 0 1 h q).
 apply AS_ContBody. apply AS_LetAssoc.
 * exact Ht.
Qed.

(* The replacement does not enter the installed frame introduced by the
 ambient continuation: the frame head is strictly above the hit cutoff. *)
Lemma admin_krepl_klift_plug (k : nat) (d : installed) (q : expr)
 (f : installed) :
 krepl_e k f (plug_d (klift_d 0 1 (klift0_d k d)) q) =
 plug_d (klift_d 0 1 (klift0_d k d)) (krepl_e k f q).
Proof.
 destruct d as [j c]. simpl.
 revert q f.
 induction c as [|c IH tail]; intros q f; simpl.
 - assert (Hneq : Nat.eqb (j + k + 1) k = false).
 { apply Nat.eqb_neq. lia. }
 rewrite Hneq. reflexivity.
 - assert (Hneq : Nat.eqb (j + k + 1) k = false).
 { apply Nat.eqb_neq. lia. }
 rewrite Hneq. f_equal.
 + f_equal.
 * specialize (IH q f). rewrite Hneq in IH.
 injection IH as IHbody. exact IHbody.
 * rewrite fs_klift_comp_e.
 replace (k + 1) with (S k) by lia.
 pose proof (proj2 admin_krepl_klift_nohit tail 0 k
 (olift_d 0 1 f)) as Htail.
 replace (k + 0) with k in Htail by lia. exact Htail.
Qed.

(* The full naturality square. [k] is the ambient continuation head and
 [S (k+cut)] is the separately bound continuation after crossing the
 inner shift and the ambient cutoff. *)
Lemma admin_let_shift_naturality :
 (forall v k cut d t,
 krepl_v k (installed_let_frame k
 (klift_e 0 1 (krepl_e (k + cut)
 (olift_d 0 1 (klift0_d k d)) (klift0_e k t))))
 (krepl_v (S (k + cut)) (klift_d 0 1 (klift0_d k d)) v) =
 krepl_v (S (k + cut)) (klift_d 0 1 (klift0_d k d))
 (krepl_v k (installed_let_frame k (klift_e 0 1 (klift0_e k t))) v)) /\
 (forall e k cut d t,
 krepl_e k (installed_let_frame k
 (klift_e 0 1 (krepl_e (k + cut)
 (olift_d 0 1 (klift0_d k d)) (klift0_e k t))))
 (krepl_e (S (k + cut)) (klift_d 0 1 (klift0_d k d)) e) =
 krepl_e (S (k + cut)) (klift_d 0 1 (klift0_d k d))
 (krepl_e k (installed_let_frame k (klift_e 0 1 (klift0_e k t))) e)).
Proof.
 apply (syntax_ind
 (fun v => forall k cut d t,
 krepl_v k (installed_let_frame k
 (klift_e 0 1 (krepl_e (k + cut)
 (olift_d 0 1 (klift0_d k d)) (klift0_e k t))))
 (krepl_v (S (k + cut)) (klift_d 0 1 (klift0_d k d)) v) =
 krepl_v (S (k + cut)) (klift_d 0 1 (klift0_d k d))
 (krepl_v k (installed_let_frame k (klift_e 0 1 (klift0_e k t))) v))
 (fun e => forall k cut d t,
 krepl_e k (installed_let_frame k
 (klift_e 0 1 (krepl_e (k + cut)
 (olift_d 0 1 (klift0_d k d)) (klift0_e k t))))
 (krepl_e (S (k + cut)) (klift_d 0 1 (klift0_d k d)) e) =
 krepl_e (S (k + cut)) (klift_d 0 1 (klift0_d k d))
 (krepl_e k (installed_let_frame k (klift_e 0 1 (klift0_e k t))) e))).
 - intros n k cut d t. reflexivity.
 - intros e IH k cut d t. simpl. f_equal.
 rewrite <- (klift_olift_e_comm 0 1 1 1
 (krepl_e (k + cut) (olift_d 0 1 (klift0_d k d)) (klift0_e k t))).
 rewrite (proj2 admin_olift_krepl (klift0_e k t) 1 1 (k + cut)
 (olift_d 0 1 (klift0_d k d))).
 rewrite <- (admin_klift_olift_d_general 0 1 0 1 (klift0_d k d)).
 rewrite admin_olift_d_comp.
 assert (Hkd : klift0_d k (olift_d 0 1 d) =
 olift_d 0 1 (klift0_d k d)).
 { unfold klift0_d. apply admin_klift_olift_d_general. }
 rewrite <- Hkd.
 assert (Hke : klift0_e k (olift_e 1 1 t) =
 olift_e 1 1 (klift0_e k t)).
 { unfold klift0_e. apply klift_olift_e_comm. }
 repeat rewrite <- Hke.
 unfold installed_let_frame.
 rewrite <- (klift_olift_e_comm 0 1 1 1 (klift0_e k t)).
 rewrite <- Hke.
 apply (IH k cut (olift_d 0 1 d) (olift_e 1 1 t)).
 - intros v IH k cut d t. simpl. f_equal. apply IH.
 - intros v IHv u IHu k cut d t. simpl. f_equal; [apply IHv|apply IHu].
 - intros a IHa u IHu k cut d t. simpl. f_equal.
 + apply IHa.
 + rewrite <- (klift_olift_e_comm 0 1 1 1
 (krepl_e (k + cut) (olift_d 0 1 (klift0_d k d)) (klift0_e k t))).
 assert (Hq : olift_e 1 1
 (krepl_e (k + cut) (olift_d 0 1 (klift0_d k d)) (klift0_e k t)) =
 krepl_e (k + cut)
 (olift_d 1 1 (olift_d 0 1 (klift0_d k d)))
 (olift_e 1 1 (klift0_e k t))).
 { apply (proj2 admin_olift_krepl (klift0_e k t) 1 1 (k + cut)
 (olift_d 0 1 (klift0_d k d))). }
 rewrite Hq.
 rewrite <- (admin_klift_olift_d_general 0 1 0 1 (klift0_d k d)).
 rewrite admin_olift_d_comp.
 assert (Hkd : klift0_d k (olift_d 0 1 d) =
 olift_d 0 1 (klift0_d k d)).
 { unfold klift0_d. apply admin_klift_olift_d_general. }
 rewrite <- Hkd.
 assert (Hke : klift0_e k (olift_e 1 1 t) =
 olift_e 1 1 (klift0_e k t)).
 { unfold klift0_e. apply klift_olift_e_comm. }
 repeat rewrite <- Hke.
 unfold installed_let_frame.
 rewrite <- (klift_olift_e_comm 0 1 1 1 (klift0_e k t)).
 rewrite <- Hke.
 apply (IHu k cut (olift_d 0 1 d) (olift_e 1 1 t)).
 - intros e IH k cut d t. simpl. f_equal.
 rewrite (admin_klift_krepl_e 0 (k + cut)
 (olift_d 0 1 (klift0_d k d)) (klift0_e k t)).
 replace (Nat.leb 0 (k + cut)) with true
 by (symmetry; apply Nat.leb_le; lia).
 rewrite (admin_klift_olift_d_general 0 1 0 1 (klift0_d k d)).
 assert (Hkd : klift0_d (S k) d =
 klift_d 0 1 (klift0_d k d)).
 { unfold klift0_d. rewrite admin_klift_add_d. f_equal. lia. }
 assert (Hke : klift0_e (S k) t =
 klift_e 0 1 (klift0_e k t)).
 { unfold klift0_e. rewrite fs_klift_comp_e. f_equal. lia. }
 rewrite <- Hkd, <- Hke.
 replace (S (k + cut)) with (S k + cut) by lia.
 replace (k + 1) with (S k) by lia.
 apply (IH (S k) cut d t).
 - intros n e IH k cut d t. simpl.
 destruct (Nat.eqb n (S (k + cut))) eqn:Hnr.
 + destruct (Nat.eqb n k) eqn:Hnk; simpl.
 * apply Nat.eqb_eq in Hnr. apply Nat.eqb_eq in Hnk. lia.
 * apply Nat.eqb_eq in Hnr. subst n.
 assert (Hks : Nat.eqb k (S (k + cut)) = false).
 { apply Nat.eqb_neq. lia. }
 simpl. rewrite Nat.eqb_refl.
 rewrite (admin_krepl_klift_plug k d
 (krepl_e (S (k + cut)) (klift_d 0 1 (klift0_d k d)) e)
 (installed_let_frame k
 (klift_e 0 1
 (krepl_e (k + cut) (olift_d 0 1 (klift0_d k d))
 (klift0_e k t))))).
 simpl. f_equal. apply IH.
 + destruct (Nat.eqb n k) eqn:Hnk; simpl.
 * apply Nat.eqb_eq in Hnk. subst n.
 assert (Hsk : Nat.eqb (S (k + cut)) k = false).
 { apply Nat.eqb_neq. lia. }
 assert (Hks : Nat.eqb k (S (k + cut)) = false).
 { apply Nat.eqb_neq. lia. }
 rewrite Nat.eqb_refl, Hks.
 assert (Htail :
 krepl_e (S (k + cut))
 (olift_d 0 1 (klift_d 0 1 (klift0_d k d)))
 (klift_e 0 1 (klift0_e k t)) =
 klift_e 0 1
 (krepl_e (k + cut) (olift_d 0 1 (klift0_d k d))
 (klift0_e k t))).
 { assert (Hdd :
 klift_d 0 1 (olift_d 0 1 (klift0_d k d)) =
 olift_d 0 1 (klift_d 0 1 (klift0_d k d))).
 { apply admin_klift_olift_d_general. }
 rewrite <- Hdd.
 replace (S (k + cut)) with
 (if Nat.leb 0 (k + cut) then S (k + cut) else k + cut)
 by (replace (Nat.leb 0 (k + cut)) with true
 by (symmetry; apply Nat.leb_le; lia); reflexivity).
 rewrite <- (admin_klift_krepl_e 0 (k + cut)
 (olift_d 0 1 (klift0_d k d)) (klift0_e k t)).
 replace (Nat.leb 0 (k + cut)) with true
 by (symmetry; apply Nat.leb_le; lia).
 reflexivity. }
 congruence.
 * rewrite Hnr, Hnk. f_equal. apply IH.
 - intros n k cut d t. simpl.
 destruct (Nat.eqb n (S (k + cut))) eqn:Hnr.
 + destruct (Nat.eqb n k) eqn:Hnk; simpl.
 * apply Nat.eqb_eq in Hnr. apply Nat.eqb_eq in Hnk. lia.
 * apply Nat.eqb_eq in Hnr. subst n. simpl.
 destruct d as [j c]. simpl.
 assert (Hneq : Nat.eqb k (S (k + cut)) = false).
 { apply Nat.eqb_neq. lia. }
 assert (Hhead : Nat.eqb (j + k + 1) k = false).
 { apply Nat.eqb_neq. lia. }
 rewrite Hhead, Nat.eqb_refl. reflexivity.
 + destruct (Nat.eqb n k) eqn:Hnk; simpl.
 * apply Nat.eqb_eq in Hnk. subst n. simpl.
 destruct d as [j c]. simpl.
 assert (Hneq : Nat.eqb k (S (k + cut)) = false).
 { apply Nat.eqb_neq. lia. }
 assert (Hhead : Nat.eqb (j + k + 1) k = false).
 { apply Nat.eqb_neq. lia. }
 rewrite Nat.eqb_refl, Hneq. reflexivity.
 * rewrite Hnr, Hnk. reflexivity.
Qed.

Lemma admin_let_shift_naturality_zero (cut : nat) (d : installed)
 (e t : expr) :
 krepl_e 0 (frame (krepl_e cut (olift_d 0 1 d) t))
 (krepl_e (S cut) (klift_d 0 1 d) e) =
 krepl_e (S cut) (klift_d 0 1 d)
 (krepl_e 0 (frame t) e).
Proof.
 pose proof ((proj2 admin_let_shift_naturality) e 0 cut d t) as H.
 unfold klift0_d, klift0_e in H.
 rewrite admin_klift_zero_d, klift_zero_e in H.
 rewrite admin_frame_eq.
 simpl in H |-.
 exact H.
Qed.

(* The two occurrences of [0] in the LetS rule are not the ambient
 continuation variable: the [EShift] on the right introduces a fresh
 continuation binder. Thus this is a lifted-substitution square, not a
 fusion equation for two frames. The ambient installed map is lifted under
 that fresh binder, while the tail payload is lifted under the ordinary
 [let] binder. *)

Lemma admin_krepl_let_shift_root (cut : nat) (d : installed)
 (e t : expr) :
 admin_step
 (krepl_e cut d (ELet (EShift e) t))
 (krepl_e cut d (EShift (krepl_e 0 (frame t) e))).
Proof.
 simpl.
 rewrite <- admin_let_shift_naturality_zero.
 apply AS_LetShift.
Qed.

(* A step in the tail changes only the payload of the installed one-let
 frame. This is the easy half of the HLetS peak. *)
Lemma admin_let_shift_tail_residual (e t t' : expr) :
 admin_step t t' ->
 joinable (admin_step)
 (EShift (krepl_e 0 (frame t) e))
 (ELet (EShift e) t').
Proof.
 intro Ht.
 assert (Hq : star (admin_step)
 (klift_e 0 1 t) (klift_e 0 1 t')).
 { apply (admin_star_map (admin_step) (admin_step)
 (klift_e 0 1)).
 - intros x y Hxy. exact (proj2 (admin_klift_step ) x y Hxy 0).
 - apply star_one. exact Ht. }
 pose proof ((proj2 (admin_krepl_frame_star ) e 0 0
 (klift_e 0 1 t) (klift_e 0 1 t') Hq)) as Hframe.
 exists (EShift (krepl_e 0 (frame t') e)); split.
 - rewrite admin_frame_eq, admin_frame_eq.
 apply (admin_star_map (admin_step) (admin_step) EShift).
 + intros x y Hxy. apply AS_ShiftBody. exact Hxy.
 + exact Hframe.
 - eapply star_step.
 + apply AS_LetShift.
 + apply star_refl.
Qed.

(* If the body step transports through the captured frame, it closes the
 other non-root branch of HLetS. *)
Lemma admin_let_shift_body_residual
 (Hbody : forall e e' t,
 admin_step e e' ->
 joinable (admin_step)
 (krepl_e 0 (frame t) e)
 (krepl_e 0 (frame t) e'))
 (e e' t : expr) :
 admin_step e e' ->
 joinable (admin_step)
 (EShift (krepl_e 0 (frame t) e))
 (ELet (EShift e') t).
Proof.
 intro He.
 destruct (Hbody e e' t He) as [w [Hw Hw']].
 exists (EShift w); split.
 - apply (admin_star_map (admin_step) (admin_step) EShift).
 + intros x y Hxy. apply AS_ShiftBody. exact Hxy.
 + exact Hw.
 - eapply star_step.
 + apply AS_LetShift.
 + apply (admin_star_map (admin_step) (admin_step) EShift).
 * intros x y Hxy. apply AS_ShiftBody. exact Hxy.
 * exact Hw'.
Qed.

(* This is the exact reduction of HLetS to the body-compatibility lemma and
 the tail-payload lemma. The remaining root branch is reflexive. *)
Lemma admin_let_shift_root_residual_from_body
 (Hbody : forall e e' t,
 admin_step e e' ->
 joinable (admin_step)
 (krepl_e 0 (frame t) e)
 (krepl_e 0 (frame t) e')) :
 forall e t z,
 admin_step (ELet (EShift e) t) z ->
 joinable (admin_step)
 (EShift (krepl_e 0 (frame t) e)) z.
Proof.
 intros e t z Hz. inversion Hz; subst.
 - inversion H2; subst.
 apply admin_let_shift_body_residual; assumption.
 - apply admin_let_shift_tail_residual; assumption.
 - exists (EShift (krepl_e 0 (frame t) e)); split; apply star_refl.
Qed.

Lemma admin_joinable_refl {A : Type} (R : A -> A -> Prop) (x : A) :
 joinable R x x.
Proof.
 exists x; split; apply star_refl.
Qed.

(* The whole body-compatibility induction is structural once the two
 genuinely continuation-sensitive tail roots are supplied. [Htail] is
 exactly the ECont-hit obligation; dL.S and A.d are both instances of it. *)
Lemma admin_installed_frame_compatibility
 (Htail : forall h q k e e',
 tail_step k e e' ->
 joinable (admin_step)
 (krepl_e h (installed_let_frame h q) (ECont k e))
 (krepl_e h (installed_let_frame h q) (ECont k e'))) :
 (forall v v', admin_vstep v v' -> forall h q,
 joinable (admin_vstep)
 (krepl_v h (installed_let_frame h q) v)
 (krepl_v h (installed_let_frame h q) v')) /\
 (forall e e', admin_step e e' -> forall h q,
 joinable (admin_step)
 (krepl_e h (installed_let_frame h q) e)
 (krepl_e h (installed_let_frame h q) e')).
Proof.
 apply admin_mutind.
 - intros e e' He IH h q. simpl.
 apply admin_joinable_lam.
 apply IH with (h := h) (q := olift_e 1 1 q).
 - intros v v' Hv IH h q. simpl.
 apply admin_joinable_val. apply IH with (h := h) (q := q).
 - intros v v' u Hv IH h q. simpl.
 apply admin_joinable_app.
 + apply IH with (h := h) (q := q).
 + apply admin_joinable_refl.
 - intros v u u' Hu IH h q. simpl.
 apply admin_joinable_app.
 + apply admin_joinable_refl.
 + apply IH with (h := h) (q := q).
 - intros a a' t Ha IH h q. simpl.
 apply admin_joinable_let.
 + apply IH with (h := h) (q := q).
 + apply admin_joinable_refl.
 - intros a t t' Ht IH h q. simpl.
 apply admin_joinable_let.
 + apply admin_joinable_refl.
 + apply IH with (h := h) (q := olift_e 1 1 q).
 - intros e e' He IH h q. simpl.
 replace (h + 1) with (S h) by lia.
 apply admin_joinable_shift.
 apply IH with (h := S h) (q := klift_e 0 1 q).
 - intros k e e' He IH h q. simpl.
 destruct (Nat.eqb k h) eqn:Hkh.
 + apply Nat.eqb_eq in Hkh. subst k.
 cbn [krepl_e].
 apply (admin_joinable_map (admin_step) (admin_step)
 (fun z => ECont h (ELet z q))).
 * intros x y Hxy. apply AS_ContBody. apply AS_LetBinding. exact Hxy.
 * apply IH with (h := h) (q := q).
 + cbn [krepl_e].
 apply admin_joinable_cont.
 apply IH with (h := h) (q := q).
 - intros k e e' Hd h q.
 exact (Htail h q k e e' Hd).
 - intros e t h q.
 exists (krepl_e h (installed_let_frame h q)
 (EShift (krepl_e 0 (frame t) e))); split.
 + apply star_one. apply admin_krepl_let_shift_root.
 + apply star_refl.
 - intros a u t h q.
 exists (krepl_e h (installed_let_frame h q)
 (ELet a (ELet u (olift_e 1 1 t)))); split.
 + apply star_one. apply admin_krepl_let_assoc_root.
 + apply star_refl.
Qed.

Corollary admin_frame_body_compatibility
 (Htail : forall h q k e e',
 tail_step k e e' ->
 joinable (admin_step)
 (krepl_e h (installed_let_frame h q) (ECont k e))
 (krepl_e h (installed_let_frame h q) (ECont k e'))) :
 forall e e' t, admin_step e e' ->
 joinable (admin_step)
 (krepl_e 0 (frame t) e)
 (krepl_e 0 (frame t) e').
Proof.
 intros e e' t He.
 pose proof ((proj2 (admin_installed_frame_compatibility Htail)
 e e' He 0 (klift_e 0 1 t))) as H.
 change (joinable (admin_step)
 (krepl_e 0 (frame t) e)
 (krepl_e 0 (frame t) e')) in H.
 exact H.
Qed.