proposition: Lemma bijective_ens_id {A : Type} (U : Ensemble A) : bijective_ens id U U.
proof: Proof. split. - intros ? ? ?. auto. - intros ? ?. exists y. auto. Qed.
imports: Coq(ClassicalChoice Description Program.Subset) ZornsLemma(DecidableDec EnsemblesImplicit Families FunctionProperties Image InverseImage Powerset_facts Proj1SigInjective) Coq(RelationClasses)