proposition: Lemma in_inter : forall x E F, x \in (E \n F) = ((x \in E) /\ (x \in F)).
proof: Proof. Proof using. unfold mem, inter. simpl. intros. rewrite in_inter_eq. autos*. Qed.
imports: TLC(LibTactics LibList) TLC(LibSet LibLogic LibEqual LibReflect)