Some ectx_language properties.

(which are useful in Amin's logical relations development).

program_logic/ectx_language.v

@@ -65,6 +65,10 @@ Section ectx_language.
       e1 = fill K e1' → e2 = fill K e2' →
       head_step e1' σ1 e2' σ2 efs → prim_step e1 σ1 e2 σ2 efs.
 
+  Lemma Ectx_step' K e1 σ1 e2 σ2 efs :
+    head_step e1 σ1 e2 σ2 efs → prim_step (fill K e1) σ1 (fill K e2) σ2 efs.
+  Proof. econstructor; eauto. Qed.
+
   Lemma val_prim_stuck e1 σ1 e2 σ2 efs :
     prim_step e1 σ1 e2 σ2 efs → to_val e1 = None.
   Proof. intros [??? -> -> ?]; eauto using fill_not_val, val_stuck. Qed.

program_logic/ectxi_language.v

@@ -46,6 +46,9 @@ Section ectxi_language.
 
   Definition fill (K : ectx) (e : expr) : expr := fold_right fill_item e K.
 
+  Lemma fill_app (K1 K2 : ectx) e : fill (K1 ++ K2) e = fill K1 (fill K2 e).
+  Proof. apply fold_right_app. Qed.
+
   Instance fill_inj K : Inj (=) (=) (fill K).
   Proof. red; induction K as [|Ki K IH]; naive_solver. Qed.
 
@@ -78,7 +81,7 @@ Section ectxi_language.
        fixed fields of different records, even when I did not. *)
     Build_EctxLanguage expr val ectx state of_val to_val [] (++) fill head_step _ _ _ _ _ _ _ _ _.
   Solve Obligations with eauto using to_of_val, of_to_val, val_stuck,
-    fill_not_val, step_by_val, fold_right_app, app_eq_nil.
+    fill_not_val, fill_app, step_by_val, fold_right_app, app_eq_nil.
 
   Global Instance ectxi_lang_ctx_item Ki :
     LanguageCtx (ectx_lang expr) (fill_item Ki).