proposition: Lemma in_remove : forall x E F, x \in (E \- F) = ((x \in E) /\ (x \notin F)).
proof: Proof. Proof using. unfold mem, remove. simpl. intros. rewrite in_remove_eq. autos*. Qed.
imports: TLC(LibTactics LibList) TLC(LibSet LibLogic LibEqual LibReflect)