proposition: Lemma rangeUn f1 f2 : range (f1 \+ f2) =i [pred x | valid (f1 \+ f2) && ((x \in range f1) || (x \in range f2))].
proof: Proof. move=>k; apply/idP/idP; last first. - case/andP=>W /orP [] /mem_seqP H; apply/mem_seqP; by [apply/(In_rangeL W) | apply/(In_rangeR W)]. move/mem_seqP=>H; rewrite (In_range_valid H) inE /=. by case/In_rangeUn: H=>/mem_seqP -> //; rewrite orbT. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)