proposition: Lemma incl_bigcapl T U A B (F : T -> set U) : B \subset A -> \bigcap_(x in A) F x \subset \bigcap_(x in B) F x.
proof: Proof. by move => Hsub t Hcap x HB; eauto. Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)