proposition: Lemma omg_morph_ax : morph_axiom omg_seprel omg.
proof: Proof. rewrite /omg; split=>[|x y V /andP [X Y]]; first by rewrite lastatval0. rewrite lastatvalUn V; case: ltngtP X Y=>H X Y; by rewrite ?(negbTE X) ?(negbTE Y) //; case: ifP. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options prelude pred) pcm(pcm morphism natmap)