proposition: Lemma setI_set0 {U} (s1 s2 : set U) : (forall x, s1 x -> ~ s2 x) -> (s1 :&: s2) <--> set0.
proof: Proof. intros; split; firstorder. Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)