Commit ed7e0be2 authored by Glen Mével's avatar Glen Mével

removed duplicated lemma

parent c6057c67
...@@ -352,13 +352,6 @@ Section Soundness. ...@@ -352,13 +352,6 @@ Section Soundness.
(* derive the adequacy of the translated program from a Hoare triple in Iris. *) (* derive the adequacy of the translated program from a Hoare triple in Iris. *)
Lemma auth_mnat_alloc `{inG Σ (authR mnatUR)} (n : mnat) :
(|==> γ, own γ (mnat n) own γ (mnat n))%I.
Proof.
by iMod (own_alloc (mnat n mnat n)) as (γ) "[? ?]" ; auto with iFrame.
Qed.
Global Arguments auth_mnat_alloc {_ _} n%nat.
Lemma spec_trtranslation__adequate_translation {Σ} (nmax : nat) (ψ : val Prop) e : Lemma spec_trtranslation__adequate_translation {Σ} (nmax : nat) (ψ : val Prop) e :
(0 < nmax)%nat (0 < nmax)%nat
( `{!timeReceiptHeapG Σ}, ( `{!timeReceiptHeapG Σ},
......
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