proposition: Lemma eq_cardinal_ens_sig {X : Type} (P : X -> Prop) : eq_cardinal_ens (@Full_set (sig P)) P.
proof: Proof. right. exists (@proj1_sig X P). split; [|split]. - intros p _. apply proj2_sig. - intros p0 p1 _ _. destruct p0, p1. apply subset_eq_compat. - intros x Hx. exists (exist P x Hx). split; [constructor|reflexivity]. Qed.
imports: Coq(ClassicalChoice Description Lia PeanoNat Program.Subset) ZornsLemma(Cardinals CountableTypes CSB DecidableDec Families Finite_sets FiniteTypes FunctionProperties FunctionPropertiesEns InverseImage Powerset_facts Proj1SigInjective ReverseMath.AddSubtract) Coq(RelationClasses)