proposition: Lemma cover_cast m n (P : {set {set 'I_n}}) (H : n = m) : cover (imset (cast_set H) (mem P)) = (cast_set H) (cover P).
proof: Proof. rewrite /= cover_imset /cover; apply: esym; apply: big_morph => [i j /=|]. - exact: imsetU. - exact: imset0. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype finfun fintype choice seq tuple) mathcomp(finset tuple bigop) tools