Commit ef040112 authored by Dan Frumin's avatar Dan Frumin

Quickfix of a rel_store_l lemma

parent 45db2579
...@@ -469,7 +469,7 @@ Section properties. ...@@ -469,7 +469,7 @@ Section properties.
Lemma bin_log_related_store_l' Δ Γ E K l e v v' t τ : Lemma bin_log_related_store_l' Δ Γ E K l e v v' t τ :
(to_val e = Some v') (to_val e = Some v')
(l ↦ᵢ v) - (l ↦ᵢ v) -
(l ↦ᵢ v' - {E,E;Δ;Γ} fill K (Lit Unit) log t : τ) (l ↦ᵢ v' - {E,E;Δ;Γ} fill K (Lit Unit) log t : τ)
- {E,E;Δ;Γ} fill K (Store (Loc l) e) log t : τ. - {E,E;Δ;Γ} fill K (Store (Loc l) e) log t : τ.
Proof. Proof.
iIntros (?) "Hl Hlog". iIntros (?) "Hl Hlog".
......
Markdown is supported
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