proposition: Lemma Cr_incl (alpha beta : Ord) (H :beta <= alpha) : Included (Cr alpha) (Cr beta).
proof: Proof. case (le_disj H). - intro;subst beta; auto with schutte. - red; intros; apply Cr_lt with alpha; auto. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Classical) ZornsLemma(CountableTypes)