proposition: Lemma domeqVUnE f1 f2 f1' f2' : dom_eq f1 f2 -> dom_eq f1' f2' -> valid (f1 \+ f1') = valid (f2 \+ f2').
proof: Proof. have L f f' g : dom_eq f f' -> valid (f \+ g) -> valid (f' \+ g). - case/domeqP=>E F; case: validUn=>// Vg1 Vf H _; case: validUn=>//. - by rewrite -E Vg1. - by rewrite Vf. by move=>x; rewrite -F; move/H/negbTE=>->. move=>H H'; case X: (valid (f1 \+ f1')); apply/esym. - by move/(L _ _ _ H): X; rewrite !(joinC f2); move/(L _ _ _ H'). rewrite domeq_sym in H; rewrite domeq_sym in H'. apply/negbTE; apply: contra (negbT X); move/(L _ _ _ H). by rewrite !(joinC f1); move/(L _ _ _ H'). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)