proposition: Lemma funsetC_mono : {homo G : X Y / X \subset Y}.
proof: Proof. by move=> *; rewrite subCset setCK F_mono// subCset setCK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)