proposition: Lemma proper_of_proper : forall B beta beta', ordinal beta -> In B beta -> In (proper_segment_of B beta) beta' -> proper_segment_of B beta' = proper_segment_of (proper_segment_of B beta) beta'.
proof: Proof. Proof with eauto with schutte. intros; apply Extensionality_Ensembles; split. - red; destruct 1; split. + split;auto. destruct H3; split. * apply lt_trans with beta'... case H1;tauto. * auto. + decompose [and] H3; split;auto. - red; destruct 1;auto. split. + case H2;auto. + split. * tauto. * destruct H3, H4 ... Qed.
imports: ZornsLemma(CountableTypes)