(* iris_heap_lang/proph_erasure.v *)
Lemma prim_step_matched_by_erased_steps_ectx_item Ki K e1 e1' σ1 e2 σ2 efs κ :
  base_step e1' (erase_state σ1) κ e2 σ2 efs →
  not_stuck e1 σ1 →
  erase_expr e1 = fill_item Ki (fill K e1') →
  (∀ K' e1, length K' ≤ length K →
     erase_expr e1 = (fill K' e1') → not_stuck e1 σ1 →
     prim_step_matched_by_erased_steps e1 σ1 (fill K' e2) σ2 efs) →
  prim_step_matched_by_erased_steps e1 σ1 (fill_item Ki (fill K e2)) σ2 efs.
Proof.
  intros Hhstp Hsf He1 IH; simpl in *.
  (** Case split on whether e1 is a [Resolve] expression. *)
  destruct (decide (is_Resolve e1)); last first.
  { (** e1 is not a [Resolve] expression. *)
    eapply non_resolve_prim_step_matched_by_erased_steps_ectx_item; [|by eauto..].
    by eapply fill_not_val, val_base_stuck. }
  (** e1 is a [Resolve] expression. *)
  destruct Ki; simplify_eq/=;
    repeat
      match goal with
      | H : erase_expr ?e = ?e' |- _ =>
        progress
          match e' with
          | fill _ _ => idtac
          | _ => destruct e; simplify_eq/=
          end
      end; try done.
  destruct K as [|Ki K _] using rev_ind; simplify_eq/=; [|].
  { (* case where (Fst (erase_expr e1_1, erase_expr e1_2, erase_expr e1_3)) *)
    (*      takes a base_step; it is impossible! *)
    by inversion Hhstp; simplify_eq. }
  rewrite /erase_resolve fill_app /= in He1; simplify_eq/=.
  destruct Ki; simplify_eq/=; rewrite fill_app /=.
  destruct K as [|Ki K _] using rev_ind; simplify_eq/=; [|].
  { (* case where (erase_expr e1_1, erase_expr e1_2, erase_expr e1_3) *)
    (*      takes a base_step; it is impossible! *)
    inversion Hhstp. }
  rewrite fill_app /= in He1.
  destruct Ki; simplify_eq/=; rewrite fill_app /=.
  - destruct K as [|Ki K _] using rev_ind; simplify_eq/=; [|].
    { (** [Resolve v0 v1 v2] is not safe! *)
      inversion Hhstp; simplify_eq/=.
      repeat
        match goal with
        | H : erase_expr ?e = _ |- _ => destruct e; simplify_eq/=
        | H : _ = erase_expr ?e |- _ => destruct e; simplify_eq/=
        end.
      by exfalso; eapply Resolve_3_vals_unsafe. }
    rewrite fill_app /= in He1.
    destruct Ki; simplify_eq/=; rewrite fill_app /=.
    + (** e1 is of the form ([Resolve] e10 e11 v0) and e11 takes a prim_step. *)
      destruct Hsf as [[? ?]| (?&?&?&?&Hrpstp)]; first done; simpl in *.
      inversion Hrpstp as [??? Hrs ? Hhstp']; simplify_eq/=.
      repeat
        match goal with
        | H : erase_expr ?e = ?e' |- _ =>
          progress
            match e' with
            | fill _ _ => idtac
            | _ => destruct e; simplify_eq/=
            end
        end.
      edestruct fill_to_resolve as [?|[K' [Ki HK]]]; eauto;
        [by eapply val_base_stuck| |]; simplify_eq/=.
      * (** e1 is of the form ([Resolve] e10 e11 v0) and e11 takes a base_step. *)
        inversion Hhstp'; simplify_eq.
        edestruct (IH K) as (?&?&?&?&?&Hpstp&?&?&?&?);
          [rewrite !length_app /=; lia|done|by eapply base_step_not_stuck|];
            simplify_eq/=.
        apply base_reducible_prim_step in Hpstp; simpl in *;
          last by rewrite /base_reducible /=; eauto 10.
        epose (λ H, base_step_to_val _ _ _ (Val _) _ _ _ _ _ _ _ H Hpstp)
          as Hhstv; edestruct Hhstv as [? ?%of_to_val]; [done|eauto|];
          simplify_eq.
        eexists _, _, _, _, _; repeat split;
          first (by apply base_prim_step; econstructor; eauto); auto.
        etrans.
        { by apply (rtc_pure_step_ctx
                      (fill [PairLCtx _; PairLCtx _; FstCtx; FstCtx])). }
        apply projs_pure_steps.
      * (** e1 is of the form ([Resolve] e10 v v0) and e10 takes a
           (non-head) prim_step. *)
        rewrite fill_app in Hrs; simplify_eq/=.
        edestruct (IH K) as (?&?&?&?&?&Hpstp&Hprstps&?&?&?);
          [rewrite !length_app; lia|done| |].
        { change (fill_item Ki) with (fill [Ki]).
          by rewrite -fill_app; eapply prim_step_not_stuck, Ectx_step. }
        simplify_eq/=.
        change (fill_item Ki) with (fill [Ki]) in Hpstp.
        rewrite -fill_app in Hpstp.
        eapply base_reducible_prim_step_ctx in Hpstp as [e2'' [He2'' Hpstp]];
          last by eexists _; eauto.
        simplify_eq/=.
        eexists _, _, _, _, _; repeat split.
        -- apply (fill_prim_step [ResolveLCtx _ _ _]); eapply Ectx_step; eauto.
        -- simpl; rewrite fill_app in Hprstps.
           by apply (rtc_pure_step_ctx
                    (fill [PairLCtx _; PairLCtx _; FstCtx; FstCtx])).
    + (** e1 is of the form ([Resolve] e1_ e1_2 v) and e1_2 takes a prim_step. *)
      repeat
        match goal with
        | H : erase_expr ?e = ?e' |- _ =>
          progress
            match e' with
            | fill _ _ => idtac
            | _ => destruct e; simplify_eq/=
            end
        end.
      apply (prim_step_matched_by_erased_steps_ectx [ResolveMCtx _ _]).
      apply IH; [rewrite !length_app /=; lia|done|
                 by eapply (not_stuck_fill_inv (fill [ResolveMCtx _ _])); simpl].
  - (** e1 is of the form ([Resolve] e1_ e1_2 e13) and e1_3 takes a prim_step. *)
    apply (prim_step_matched_by_erased_steps_ectx [ResolveRCtx _ _]).
    apply IH; [rewrite !length_app /=; lia|done|
                 by eapply (not_stuck_fill_inv (fill [ResolveRCtx _ _])); simpl].
Qed.