proposition: Lemma injective_injective_ens : injective f -> injective_ens.
proof: Proof. intros Hf x0 x1 _ _; apply Hf; auto. Qed.
imports: Coq(ClassicalChoice Description Program.Subset) ZornsLemma(DecidableDec EnsemblesImplicit Families FunctionProperties Image InverseImage Powerset_facts Proj1SigInjective) Coq(RelationClasses)