proposition: Lemma cvgi_app U V (F G : set_system U) (f : U -> set V) : F --> G -> f `@ F --> f `@ G.
proof: Proof. by move=> FG P /=; exact: FG. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed