add lemma about readucing ectxi-languages

program_logic/ectxi_language.v

@@ -86,4 +86,17 @@ Section ectxi_language.
   Global Instance ectxi_lang_ctx_item Ki :
     LanguageCtx (ectx_lang expr) (fill_item Ki).
   Proof. change (LanguageCtx _ (fill [Ki])). apply _. Qed.
+
+  Lemma step_is_head K e σ :
+    to_val e = None → (∀ Ki K e', e = fill (Ki::K) e' → ¬head_reducible e' σ) →
+    reducible (fill K e) σ → head_reducible e σ.
+  Proof.
+    intros Hnonval Hnondecomp (e'&σ''&ef&Hstep).
+    change fill with ectx_language.fill in Hstep.
+    apply fill_step_inv in Hstep; last done. destruct Hstep as (e2'&_&Hstep).
+    clear K. destruct Hstep as [K e1' e2'' ?? Hstep]. subst.
+    destruct K as [|K0 K].
+    { rewrite fill_empty in Hnonval. subst. eexists; eauto. }
+    exfalso. eapply Hnondecomp; first done. do 3 eexists. done.
+  Qed.
 End ectxi_language.