proposition: Lemma injective_ens_char (H : range) : injective_ens <-> injective (range_restr H).
proof: Proof. split. - intros H0 [x0 Hx0] [x1 Hx1] Hx. simpl in *. specialize (H0 x0 x1 Hx0 Hx1). inversion Hx; subst; clear Hx. apply subset_eq_compat. auto. - intros H0 x0 x1 Hx0 Hx1 Heq. specialize (H0 (exist _ x0 Hx0) (exist _ x1 Hx1)). simpl in H0. unshelve epose proof (H0 _) as H0. { apply subset_eq_compat. assumption. } inversion H0; subst; clear H0. reflexivity. Qed.
imports: Coq(ClassicalChoice Description Program.Subset) ZornsLemma(DecidableDec EnsemblesImplicit Families FunctionProperties Image InverseImage Powerset_facts Proj1SigInjective) Coq(RelationClasses)