proposition: Lemma validUnAE f1 f2 : valid (f1 \+ f2) = [&& valid f1, valid f2 & all [predC dom f1] (dom f2)].
proof: Proof. apply/idP/idP. - case: validUn=>// ->-> H _; apply/allP=>k. by apply: contraL (H _). case/and3P=>V1 V2 /allP /= D; case: validUn=>//. - by rewrite V1. - by rewrite V2. by move=>k X1 X2; move: (D k X2); rewrite X1. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)