Commit cbeb20a2 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Fix persistent_dup_L.

parent 53fe9f40
......@@ -575,7 +575,7 @@ Section cmra_leibniz.
Proof. unfold_leibniz. apply cmra_pcore_dup'. Qed.
(** ** Persistent elements *)
Lemma persistent_dup_L x `{!Persistent x} : x x x.
Lemma persistent_dup_L x `{!Persistent x} : x = x x.
Proof. unfold_leibniz. by apply persistent_dup. Qed.
(** ** Total core *)
Supports Markdown
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