proposition: Lemma test_neq_solve : forall x y E F, x \notin (E \u \{y} \u F) -> y \notin E -> y <> x /\ x <> y.
proof: Proof. Proof using. split. notin_solve. notin_solve. Qed.
imports: TLC(LibTactics) TLC(LibLogic LibEqual LibList LibRelation LibWf LibList LibLN)