proposition: Lemma bigcap_set1 {U T} (x : U) (f : U -> set T) : bigcap [set x] f <--> f x.
proof: Proof. split; move => H. eapply H. reflexivity. intros y Hy. inversion Hy. subst. assumption. Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)