fix a couple of admits

theories/typing/contextual_refinement.v

@@ -325,6 +325,7 @@ Definition ctx_refines_alt (Γ : stringmap type)
 (*   econstructor. eapply step_atomic with (t1 := []); eauto. *)
 (* Qed. *)
 
+(* Helper lemmas *)
 Lemma erased_step_ectx (e e' : expr) tp tp' σ σ' K :
   erased_step (e :: tp, σ) (e' :: tp', σ') →
   erased_step ((fill K e) :: tp, σ) (fill K e' :: tp', σ').
@@ -387,6 +388,23 @@ Proof.
     by eapply erased_step_ectx.
 Qed.
 
+Lemma rtc_erased_step_smart_ctx (e : expr) σ0 σ1 tp0 tp1 :
+  rtc erased_step ((e ;; #true)%E :: tp0, σ0) (of_val #true :: tp1, σ1) →
+  ∃ (v : val), rtc erased_step (e :: tp0, σ0) (of_val v :: tp1, σ1).
+Proof.
+  pose (P := λ (s1 s2 : list expr * state),
+             match s1, s2 with
+             | ((Seq e #true)%E :: tp0, σ0), (of_val #true :: tp1, σ1) =>
+               ∃ (v : val), rtc erased_step (e :: tp0, σ0) (of_val v :: tp1, σ1)
+             | _,_ => True
+             end).
+  (* eapply (rtc_ind _ P); clear tp0 tp1 σ0 σ1. *)
+  (* - intros [tp σ]. unfold P. *)
+  (*   destruct tp as [|e' tp]; first done. *)
+  (*   repeat (case_match; eauto). *)
+  admit.
+Admitted.
+
 Lemma ctx_refines_impl_alt Γ e1 e2 τ :
   (Γ ⊨ e1 ≤ctx≤ e2 : τ) →
   ctx_refines_alt Γ e1 e2 τ.
@@ -399,7 +417,7 @@ Proof.
   - unfold C'; simpl.
     destruct 1 as (thp' & σ1' & Hstep').
     exists thp', σ1'.
-    admit.
+    eapply rtc_erased_step_smart_ctx. done.
   - eapply (H C' thp _ σ1 #true TBool).
     + repeat econstructor; eauto.
     + repeat econstructor; eauto.
@@ -408,13 +426,18 @@ Proof.
       { econstructor.
         - econstructor.
           eapply (step_atomic) with (t1 := []); try reflexivity.
-          admit.
-        - admit. }
+          eapply Ectx_step with (K:=[AppLCtx v1]); try reflexivity.
+          econstructor.
+        - eapply rtc_once. rewrite app_nil_r. econstructor.
+          eapply (step_atomic) with (efs:=[]) (t1 := []); try reflexivity.
+          { rewrite /= app_nil_r //. }
+          eapply Ectx_step with (K:=[]); try reflexivity.
+          by econstructor. }
       pose (K := [AppRCtx (λ: <>, #true)%E]).
       change (fill_ctx C e1;; #true)%E with (fill K (fill_ctx C e1)).
       change (v1;; #true)%E with (fill K (of_val v1)).
       by eapply rtc_erased_step_ectx.
-Admitted.
+Qed.
 
 Definition ctx_equiv Γ e1 e2 τ :=
   (Γ ⊨ e1 ≤ctx≤ e2 : τ) ∧ (Γ ⊨ e2 ≤ctx≤ e1 : τ).