proposition: Lemma big_domeq2Un A (xs : seq A) (f1 : A -> U1) (f2 : A -> U2) : (forall x, x \In xs -> dom_eq2 (f1 x) (f2 x)) -> dom_eq2 (\big[PCM.join/Unit]_(i <- xs) (f1 i)) (\big[PCM.join/Unit]_(i <- xs) (f2 i)).
proof: Proof. elim: xs=>[|x xs IH] D; first by rewrite !big_nil domeq2_unit. rewrite !big_cons; apply: domeq2Un. - by apply: D; rewrite InE; left. by apply: IH=>z Z; apply: D; rewrite InE; right. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)