Prove `subst_p_det` without admits

Thanks to Robbert

theories/F_mu_ref_conc/subst.v

@@ -490,14 +490,12 @@ Proof.
   apply subst_p_head_step; eauto.
 Qed.
 
-Lemma subst_p_det_head e e' es :
-  (∀ σ, head_step e σ e' σ []) →
-  (∀ σ1 e2 σ2 efs, head_step e σ1 e2 σ2 efs -> σ1=σ2 /\ e'=e2 /\ [] = efs) →
-  (∀ σ1 e2 σ2 efs, head_step (subst_p es e) σ1 e2 σ2 efs -> σ1=σ2 /\ (subst_p es e')=e2 /\ [] = efs).
+Lemma subst_p_det_head e e' es σ1 σ2 efs :
+  head_step e σ1 e' σ1 [] →
+  (∀ e2, head_step e σ1 e2 σ2 efs -> σ1=σ2 /\ e'=e2 /\ [] = efs) →
+  (∀ e2, head_step (subst_p es e) σ1 e2 σ2 efs -> σ1=σ2 /\ (subst_p es e')=e2 /\ [] = efs).
 Proof.
-  intros Hstep Hdet σ1 e2 σ2 efs Hst.
-  specialize (Hdet σ1).
-  specialize (Hstep σ1).
+  intros Hstep Hdet e2 Hst.
   inversion Hstep; subst; simplify_eq/=;
     simpl in Hst; inversion Hst; simplify_eq/=; eauto;
   repeat lazymatch goal with
@@ -517,11 +515,11 @@ Proof.
     rewrite (Closed_subst_p_id' _ _ e1); eauto.
     rewrite (to_val_subst_p e0 v0 _); eauto.
     apply elem_of_rec_lookup.
-  - destruct (Hdet _ _ _ Hst) as (?&?&?).
+  - destruct (Hdet _ Hst) as (?&?&?).
     by simplify_eq.
-  - destruct (Hdet _ _ _ Hst) as (?&?&?).
+  - destruct (Hdet _ Hst) as (?&?&?).
     by simplify_eq.
-  - destruct (Hdet _ _ _ Hst) as (?&?&?).
+  - destruct (Hdet _ Hst) as (?&?&?).
     by simplify_eq.
 Qed.
 
@@ -529,67 +527,24 @@ Lemma subst_p_det e e' es :
   (∀ σ, prim_step e σ e' σ []) →
   (∀ σ1 e2 σ2 efs, prim_step e σ1 e2 σ2 efs -> σ1=σ2 /\ e'=e2 /\ [] = efs) →
   (∀ σ1 e2 σ2 efs, prim_step (subst_p es e) σ1 e2 σ2 efs -> σ1=σ2 /\ (subst_p es e')=e2 /\ [] = efs).
-Proof. admit. Admitted.
-  (* intros Hstep Hdet σ1 e2 σ2 efs Hst. *)
-  (* assert (Hstep' := Hstep). *)
-  (* specialize (Hdet σ1). *)
-  (* specialize (Hstep σ1). *)
-  (* destruct Hstep as [K0 e0 e0' ?? Hstep]. subst. simpl in *. *)
-  (* rewrite fill_subst in Hst. *)
-  (* rewrite fill_subst. *)
-  (* destruct Hst as [K1 t0 t2 Hfill ? Hst]. subst. simpl in *. *)
-  (* assert (to_val (subst_p es e0) = None) as Hnoval. *)
-  (* { pose (Hstuck:=val_prim_stuck). *)
-  (*   simpl in Hstuck. *)
-  (*   eapply Hstuck. *)
-  (*   apply head_prim_step. *)
-  (*   by apply subst_p_head_step. } *)
-  (* destruct (step_by_val _ _ _ _ _ _ _ _ Hfill Hnoval Hst) *)
-  (*   as [K2 Hctx]. subst. clear Hnoval. *)
-  (* rewrite fill_app in Hfill. *)
-  (* apply fill_inj in Hfill. *)
-  (* rewrite fill_app.     *)
-  (* inversion Hstep; subst; simplify_eq/=. *)
-  (* Focus 3. *)
-  (* inversion Hst; subst; simplify_eq/=. *)
-  (* split_and!; eauto. *)
-  (* f_equal. *)
-  (* rewrite -(of_to_val _ _ H0). *)
-  (* rewrite -(of_to_val _ _ H1). *)
-  
-  (* inversion Hstep; subst; simplify_eq/=. *)
-  (* inversion Hfill. *)
-  (* apply fill_inj. *)
-  (* repeat (split; eauto). *)
-  (* apply *)
-  (* simpl in Hst. *)
-  (* simpl in Hst. *)
-  (*   simpl in Hst; inversion Hst; simplify_eq/=; eauto; *)
-
-  (* inversion Hstep; subst; simplify_eq/=; *)
-  (*   simpl in Hst; inversion Hst; simplify_eq/=; eauto; *)
-  (* repeat lazymatch goal with *)
-  (* | [ H : to_val ?e = Some ?v, H' : to_val (subst_p es ?e) = Some ?v2 |- _ ] => *)
-  (*   rewrite -(of_to_val _ _ H) in H'; *)
-  (*   rewrite of_val_subst_p in H'; *)
-  (*   rewrite to_of_val in H' *)
-  (* | [ H : to_val ?e = Some ?v, H' : context[subst_p _ ?e] |- _ ] => *)
-  (*   rewrite -(of_to_val _ _ H) in H'; *)
-  (*   rewrite of_val_subst_p in H'; *)
-  (*   rewrite (of_to_val _ _ H) in H' *)
-  (* end; simplify_eq/=; *)
-  (* rewrite ?of_val_subst_p; *)
-  (* split_and !; eauto. *)
-  (* - rewrite !subst_p_delete. *)
-  (*   rewrite !(delete_commute_binder _ f x). *)
-  (*   rewrite (Closed_subst_p_id' _ _ e1); eauto. *)
-  (*   rewrite (to_val_subst_p e0 v0 _); eauto. *)
-  (*   apply elem_of_rec_lookup. *)
-  (* - destruct (Hdet _ _ _ Hst) as (?&?&?). *)
-  (*   by simplify_eq. *)
-  (* - destruct (Hdet _ _ _ Hst) as (?&?&?). *)
-  (*   by simplify_eq. *)
-  (* - destruct (Hdet _ _ _ Hst) as (?&?&?). *)
-  (*   by simplify_eq. *)
-
-  (* apply subst_p_det_head. *)
+Proof.
+  intros Hstep Hdet σ1 e2 σ2 efs Hsstep.
+  destruct Hsstep as [K e1' e2' ???]; simplify_eq/=.
+  destruct (Hstep σ1) as [K' e1'' e2'' ???]; simplify_eq/=.
+  rewrite fill_subst in H.
+  assert (K = (subst_ctx es K')) as ->.
+  { eapply (subst_p_head_step _ _ es) in H3.
+    edestruct (step_by_val K (subst_ctx es K') e1' (subst_p es e1''))
+      as [K1 ?]; eauto using val_stuck.
+    edestruct (step_by_val (subst_ctx es K') K (subst_p es e1'') e1')
+      as [[|??] ->]; eauto using val_stuck; discriminate_list. }
+  apply fill_inj in H; subst.
+  rewrite fill_subst.
+  cut (σ1 = σ2 ∧ subst_p es e2'' = e2' ∧ [] = efs).
+  { naive_solver. }
+  eapply subst_p_det_head. eauto. 2: eauto.
+  intros e2 ?.
+  destruct (Hdet σ1 (fill K' e2) σ2 efs) as (?&?%fill_inj&?).
+  { by econstructor. }
+  done.
+Qed.