proposition: Lemma Singleton_injective {T : Type} : forall x y : T, Singleton x = Singleton y -> x = y.
proof: Proof. intros. assert (In (Singleton x) x) by constructor. rewrite H in H0. now destruct H0. Qed.
imports: ZornsLemma(FunctionProperties) Coq(RelationClasses)