proposition: Lemma injective_ens_empty {X Y : Type} (f : X -> Y) : injective_ens f Empty_set.
proof: Proof. intros ? ? ?. contradiction. Qed.
imports: Coq(ClassicalChoice Description Program.Subset) ZornsLemma(DecidableDec EnsemblesImplicit Families FunctionProperties Image InverseImage Powerset_facts Proj1SigInjective) Coq(RelationClasses)