proposition: Lemma bigcapsP U P F : reflect (forall i, P i -> U \subset F i) (U \subset \bigcap_(i | P i) F i).
proof: Proof. apply: (iffP idP) => [sUF i Pi | sUF]. by apply: subset_trans sUF _; apply: bigcap_inf. elim/big_rec: _ => [|i V Pi sUV]; apply/subsetP=> x Ux; rewrite inE //. by rewrite !(subsetP _ x Ux) ?sUF. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)