proposition: Lemma test_notin_solve_2 : forall x y E F G, x \notin E \u \{y} \u F -> x \notin G -> 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)