fact: Definition bigcap (A : set T) (F : T -> set U) := [set x | forall (i : T), i \in A -> x \in F i].
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)