Skip to content
Snippets Groups Projects
Commit 4dbfd13e authored by Dan Frumin's avatar Dan Frumin
Browse files

Apply suggestion to theories/program_logic/ectx_language.v

parent 1735272a
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/program_logic/ectx_language.v
+ 1
− 1
View file @ 4dbfd13e
...@@ -179,7 +179,7 @@ Section ectx_language. ...@@ -179,7 +179,7 @@ Section ectx_language.
Proof. Proof.
rewrite -not_reducible -not_head_reducible. eauto using head_prim_reducible. rewrite -not_reducible -not_head_reducible. eauto using head_prim_reducible.
Qed. Qed.
Lemma head_prim_fill_reducible_no_obs e K σ : Lemma head_prim_fill_reducible_no_obs e K σ :
head_reducible_no_obs e σ → reducible_no_obs (fill K e) σ. head_reducible_no_obs e σ → reducible_no_obs (fill K e) σ.
Proof. intro. by apply fill_reducible_no_obs, head_prim_reducible_no_obs. Qed. Proof. intro. by apply fill_reducible_no_obs, head_prim_reducible_no_obs. Qed.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment