proposition: Lemma members_proper (alpha : Ord) : proper_segment (members alpha).
proof: Proof. Proof with eauto with schutte. split. - intros a b H H0; apply lt_trans with a ... - intros [H0 H1]; destruct (@le_not_gt alpha (succ alpha)) ... + apply (H1 (succ alpha)) ... Qed.
imports: ZornsLemma(CountableTypes)