proposition: Lemma test_notin_false_1 : forall x y E F G, x \notin (E \u \{x} \u F) -> y \notin G.
proof: Proof. Proof using. intros. dup 3. false. notin_false. notin_false. notin_false. Qed.
imports: TLC(LibTactics) TLC(LibLogic LibEqual LibList LibRelation LibWf LibList LibLN)