Alternative definition of contextual refinement

On request from @robbertkrebbers

theories/typing/contextual_refinement.v

@@ -241,7+241,7 @@
 (* Observable types are, at the moment, exactly the types which support equality. *)
 Definition ObsType : type → Prop := EqType.
 
 Definition ctx_refines (Γ : stringmap type)
     (e e' : expr) (τ : type) : Prop := ∀ K thp σ₀ σ₁ v τ',
   ObsType τ' →
   typed_ctx K Γ τ ∅ τ' →
@@ -303,7+303,7 @@
   eapply typed_ctx_compose; eauto.
 Qed.
 
+(* Alternative formulation of contextual refinement
+without restricting to contexts of the ground type *)
+Definition ctx_refines_alt (Γ : stringmap type)
+    (e e' : expr) (τ : type) : Prop := ∀ K thp σ₀ σ₁ v1 τ',
+  typed_ctx K Γ τ ∅ τ' →
+  rtc erased_step ([fill_ctx K e], σ₀) (of_val v1 :: thp, σ₁) →
+  ∃ thp' σ₁' v2, rtc erased_step ([fill_ctx K e'], σ₀) (of_val v2 :: thp', σ₁').
+
+Lemma ctx_refines_impl_alt Γ e1 e2 τ :
+  (Γ ⊨ e1 ≤ctx≤ e2 : τ) →
+  ctx_refines_alt Γ e1 e2 τ.
+Proof.
+  intros H C thp σ0 σ1 v1 τ' HC Hstep.
+  pose (C' := (CTX_AppR (λ: <>, #true)%E)::C).
+  cut (∃ (thp' : list expr) σ₁',
+              rtc erased_step ([fill_ctx C' e2], σ0)
+                (of_val #true :: thp', σ₁')).
+  - unfold C'; simpl.
+    destruct 1 as (thp' & σ1' & Hstep').
+    exists thp', σ1'.
+    admit.
+  - eapply (H C' thp _ σ1 #true TBool).
+    + repeat econstructor; eauto.
+    + repeat econstructor; eauto.
+    + unfold C'. simpl.
+      admit.
+Admitted.
 
 Definition ctx_equiv Γ e1 e2 τ :=
   (Γ ⊨ e1 ≤ctx≤ e2 : τ) ∧ (Γ ⊨ e2 ≤ctx≤ e1 : τ).