proposition: Lemma test_notin_by_auto : forall x E F G, x \notin E \u F -> x \notin G -> x \notin (E \u G).
proof: Proof. Proof using. auto. Qed.
imports: TLC(LibTactics) TLC(LibLogic LibEqual LibList LibRelation LibWf LibList LibLN)