proposition: Lemma A1_A2 :forall a, In A1 a -> A2 a /\ f1 a = f2 a.
proof: Proof. Proof with eauto with schutte. intros a Ha; generalize Ha;pattern a; apply transfinite_induction. { clear a Ha ; intros a H0 Ha ; assert (A2 a). { assert (forall khi, khi < a -> A2 khi /\ f1 khi = f2 khi). { intros; apply H0... } apply NNPP; intro H2. assert (forall y, A2 y -> y < a). { intros y H3; tricho y a H4 ... subst y; now case H2. destruct H2; apply segment_lt with y;auto with schutte. } assert (forall y, A2 y -> f1 y < f1 a). { intros y H4; case O1;intros H5 H6 H7 H8. apply H8 ... } case O2;intros H5 H6 H7 H8; case (H7 (f1 a)). - case O1;intros H9 H10 H11 H12. apply H10; auto. - destruct 1. generalize (H3 x H4). intro; case (H0 x)... + intros H13 H14. specialize (H6 _ H4). rewrite <- H9 in H10. rewrite H14 in H10. case (@lt_irrefl (f2 x));auto. } { split; trivial. assert (H01 : least_member lt (fun x => B x /\ forall y, y < a -> f1 y <> x) (f1 a)). { split. + case O1;intros; unfold In; intuition. apply OF_total0; auto. specialize (OF_mono0 y a ). assert (In A1 y) by (eapply OF_segment0 with a ; auto). specialize (OF_mono0 H3 Ha H1). rewrite H2 in OF_mono0; now apply (@lt_irrefl (f1 a)). + destruct 1; destruct O1 as [H3 H4 H5 H6]. destruct (H5 x H1). destruct H7; subst x; tricho a x0 H9. * right. apply H6;auto. * subst x0; now left. * now destruct (H2 _ H9). } assert (H02 : least_member lt (fun x => B x /\ forall y, y < a -> f2 y <> x) (f2 a)). { split. + case O2;intros H2 H3 H4 H5. unfold In; intuition. apply H3; auto. specialize (H5 y a ). assert (In A2 y) by ( eapply H2 with a ; auto). specialize (H5 H7 H H1). rewrite H6 in H5; now apply (@lt_irrefl (f2 a)). + destruct 1; case O2; intros H3 H4 H5 H6. destruct (H5 x H1). destruct H7; subst x; tricho a x0 H9. * right; apply H6;auto. * subst x0; now left. * specialize (H2 _ H9); now destruct H2. } refine (least_member_of_eq AX1 _ _ H01 H02). - intros x Hx; split. + red in Hx; tauto. + intros y H1; destruct (H0 _ H1). * case O1; intros H2 H3 H4 H5. apply H2 with a; auto. * rewrite <- H3; destruct Hx; auto. - intros x Hx; split. + red in Hx; tauto. + intros y H1; destruct (H0 _ H1). case O1;intros H2 H3 H4 H5. apply H2 with a; auto. rewrite H3; destruct Hx; auto. } } Qed.
imports: ZornsLemma(CountableTypes)