proposition: Lemma domeq2VUnE (f1 f1' : U1) (f2 f2' : U2) : dom_eq2 f1 f2 -> dom_eq2 f1' f2' -> valid (f1 \+ f1') = valid (f2 \+ f2').
proof: Proof. suff L (C1' C2' : pred K) V1' V2' (U1' : union_map_class C1' V1') (U2' : union_map_class C2' V2') (g1 g1' : U1') (g2 g2' : U2') : dom_eq2 g1 g2 -> dom_eq2 g1' g2' -> valid (g1 \+ g1') -> valid (g2 \+ g2'). - by move=>D D'; apply/idP/idP; apply: L=>//; apply: domeq2_sym. case/andP=>/eqP E /eqP D /andP [/eqP E' /eqP D']; case: validUn=>// V V' G _. case: validUn=>//; rewrite -?E ?V -?E' ?V' //. by move=>k; rewrite -D -D'=>/G/negbTE ->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)