proposition: Lemma domeq2VUn (f1 f1' : U1) (f2 f2' : U2) : dom_eq2 f1 f2 -> dom_eq2 f1' f2' -> valid (f1 \+ f1') -> valid (f2 \+ f2').
proof: Proof. by move=>D D'; rewrite -(domeq2VUnE D D'). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)