proposition: Lemma g_unic : forall g_beta g_beta', ordinal g_beta -> ordinal g_beta' -> _A = members g_beta -> _A = members g_beta' -> g_beta = g_beta'.
proof: Proof. intros g_beta g_beta' H H0 H1 H2; rewrite H2 in H1;clear H2. assert (Same_set (members g_beta') (members g_beta)). { rewrite H1; split;auto with schutte. } case H2; unfold Included, members; intros; apply le_antisym. - apply not_gt_le; auto with schutte. intro H5; generalize (H4 g_beta'); intros H6; unfold In in H6. case (@lt_irrefl g_beta'); now apply H6. - apply not_gt_le; auto with schutte. intro H5; generalize (H3 g_beta);intros H6; destruct (@lt_irrefl g_beta); now apply H6. Qed.
imports: ZornsLemma(CountableTypes)