proposition: Lemma omgidNegMorph (v1 v2 : U) : valid (v1 \+ v2) -> omg_s v1 v2 -> ~~last_atval false (v1 \+ v2) = (omg v1 \+ omg v2 == nown).
proof: Proof. by move=>W S; rewrite (@omgNegMorph _ _ _ _ (id_morph _)). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options prelude pred) pcm(pcm morphism natmap)