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