proposition: Lemma test_not_In_conj : forall x y s1 s2 s3 s4, ~ In x (union s1 (union s2 (union s3 (add y s4)))) -> ~ In x s1 /\ ~ In x s4 /\ ~ E.eq y x.
proof: Proof. fsetdec. Qed.
imports: Decidable Setoid DecidableTypeEx MSetFacts