proposition: Lemma reindex_bigcup I J K (h : J -> I) (F : I -> set K) A B : h @: B <--> A -> \bigcup_(x in A) F x <--> \bigcup_(y in B) F (h y).
proof: Proof. move=> surj t; split. case=> x [Ax Fxt]; case: (surj x) => [?]. by case=> // y [By eq_hyx]; exists y; rewrite eq_hyx. case=> y [By Fhyt]; exists (h y); split=> //. by case: (surj (h y)) => Ahy _; apply: Ahy; exists y. Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)