proposition: Lemma omgNegMorph (V : pcm) (v1 v2 : V) (D : sep_rel V) (ht : @morphism V U D) : valid (v1 \+ v2) ->'preim ht omg_s v1 v2 -> ~~ last_atval false (ht v1 \+ ht v2) = (omg (ht v1) \+ omg (ht v2) == nown).
proof: Proof. move=>W /andP [G] /andP []; rewrite /= /omg in G *. rewrite lastatvalUn (pfVf ht W G); case: ltngtP=>H H1 H2; by rewrite ?(negbTE H1) ?(negbTE H2) //; case: ifP. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options prelude pred) pcm(pcm morphism natmap)