proposition: Lemma bigcap_set0 (T U : Type) (F : T -> set U) : \bigcap_(x in set0) F x <--> setT.
proof: Proof. split. - move => _. constructor. - move => _ x H. inversion H. Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)