proposition: Lemma disjoint_in_notin : forall E F x, disjoint E F -> x \in E -> x \notin F.
proof: Proof. Proof using. unfold disjoint. introv H InE InF. applys in_empty_inv x. rewrite <- H. rewrite in_inter. auto. Qed.
imports: TLC(LibTactics LibList) TLC(LibSet LibLogic LibEqual LibReflect)