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