proposition: Lemma Cr_zero_AP : Cr zero = AP.
proof: Proof. apply Extensionality_Ensembles; split. - red; intros; red; apply Cr_zero_inv; auto. - red; intros; apply Cr_zero; auto. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Classical) ZornsLemma(CountableTypes)