proposition: Lemma finI_filter (I : choiceType) T (D : set I) (f : I -> set T) : finI D f -> ProperFilter (filter_from (finI_from D f) id).
proof: Proof. move=> finIf; apply: (filter_from_proper (filter_from_filter _ _)). - by exists setT; exists fset0 => //; rewrite predeqE. - move=> A B [DA sDA IfA] [DB sDB IfB]; exists (A `&` B) => //. exists (DA `|` DB)%fset. by move=> ?; rewrite inE => /orP [/sDA|/sDB]. rewrite -IfA -IfB predeqE => p; split=> [Ifp|[IfAp IfBp] i]. by split=> i Di; apply: Ifp; rewrite /= inE Di // orbC. by rewrite /= inE => /orP []; [apply: IfAp|apply: IfBp]. - by move=> _ [?? <-]; apply: finIf. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed