proposition: Lemma domeqP f1 f2 : reflect (valid f1 = valid f2 /\ dom f1 =i dom f2) (dom_eq f1 f2).
proof: Proof. rewrite !pcmE /= !umEX /UM.valid /UM.dom /UM.dom_eq /in_mem. case: (UMC.from f1) (UMC.from f2)=>[|f1' F1][|f2' F2] /=. - by constructor. - by constructor; case. - by constructor; case. by case: eqP=>H; constructor; [rewrite H | case=>_ /suppE]. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)