proposition: Lemma notin_union : forall x E F, x \notin (E \u F) <-> (x \notin E) /\ (x \notin F).
proof: Proof. Proof using. unfold notin. intros. rewrite* in_union. Qed.
imports: TLC(LibTactics LibList) TLC(LibSet LibLogic LibEqual LibReflect)