proposition: Lemma imset_trivIset (P : {set {set T1}}) : trivIset P -> trivIset ((fun s : {set T1} => f @: s) @: P).
proof: Proof. move=> /trivIsetP Htriv. apply/trivIsetP => A B /imsetP[FA FAP -> {A}] /imsetP[FB FBP -> {B}] Hneq. have {Hneq} neqFAFB : FA != FB by move: Hneq; apply: contra => /eqP ->. have:= Htriv _ _ FAP FBP neqFAFB; rewrite -!setI_eq0 -imsetI. - by move=> /eqP ->; rewrite imset0. - by move=> i j _ _ /=; exact: f_inj. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(finset bigop path binomial)