proposition: Lemma domeq2E (f1 : U1) (f2 : U2) : dom_eq2 f1 f2 -> (valid f1 = valid f2) * (dom f1 = dom f2).
proof: Proof. by move=>H; rewrite (domeq2VE H) (domeq2DE H). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)