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