proposition: Lemma omg_fresh_val (V : pcm) (v1 v2 : V) (D : sep_rel V) (ht : @morphism V U D) : valid (v1 \+ v2) -> D v1 v2 -> (omg (fresh (ht v1 \+ ht v2) \-> (false, true) \+ ht v1) = own) * (omg (fresh (ht v1 \+ ht v2) \-> (true, false) \+ ht v1) = nown) * (omg (fresh (ht v1 \+ ht v2) \-> (false, true) \+ ht v2) = own) * (omg (fresh (ht v1 \+ ht v2) \-> (true, false) \+ ht v2) = nown).
proof: Proof. move=>A O; have Vh : valid (ht v1 \+ ht v2). - by move/pfV2: O; move/(_ _ ht A). by rewrite /omg !lastatval_freshUn. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options prelude pred) pcm(pcm morphism natmap)