proposition: Lemma test_solve_notin_2 : forall x y E F G, ~ In x (union E (union (singleton y) F)) -> ~ In x G -> ~ In x (singleton y) /\ ~ In y (singleton x).
proof: Proof. split. solve_notin. solve_notin. Qed.
imports: Coq.FSets.FSetInterface Metalib.CoqFSetDecide