From 6645a150911a0cefc6414864e454df4bed28a6e0 Mon Sep 17 00:00:00 2001
From: Hoang-Hai Dang <haidang@mpi-sws.org>
Date: Thu, 20 Jun 2019 14:54:06 +0200
Subject: [PATCH] Add stuck_fill lemma.

---
 theories/program_logic/language.v | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/theories/program_logic/language.v b/theories/program_logic/language.v
index a1a6b7c6d..60d95f5b9 100644
--- a/theories/program_logic/language.v
+++ b/theories/program_logic/language.v
@@ -161,6 +161,12 @@ Section language.
     to_val e = None → irreducible e σ → irreducible (K e) σ.
   Proof. rewrite -!not_reducible. naive_solver eauto using reducible_fill. Qed.
 
+  Lemma stuck_fill `{!@LanguageCtx Λ K} e σ :
+    stuck e σ → stuck (K e) σ.
+  Proof.
+    intros ST. split; [by apply fill_not_val, ST|apply irreducible_fill; apply ST].
+  Qed.
+
   Lemma step_Permutation (t1 t1' t2 : list (expr Λ)) κ σ1 σ2 :
     t1 ≡ₚ t1' → step (t1,σ1) κ (t2,σ2) → ∃ t2', t2 ≡ₚ t2' ∧ step (t1',σ1) κ (t2',σ2).
   Proof.
-- 
GitLab