proposition: Lemma Lemma5_2 : forall xi eta, xi < alpha -> In M eta -> phi xi eta = eta.
proof: Proof. intros. Check (Cr_pos_iff alpha_pos). assert (Cr alpha eta). now apply IM. rewrite (Cr_pos_iff alpha_pos) in H1. now destruct (H1 _ H). Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Classical) ZornsLemma(CountableTypes)