proposition: Lemma omgPos (V : pcm) (v : V) (ht : V -> natmap (bool * bool)) : last_atval false (ht v) = (omg (ht v) == own).
proof: Proof. by rewrite /omg /=; case: ifP. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options prelude pred) pcm(pcm morphism natmap)