proposition: Lemma tower_is_chain: chain tower.
proof: Proof. unfold chain. intros. revert x H. induction H0. - intros. case (classic (forall y:T, In S y -> R y x)). + right. now apply (proj2_sig (chain_sup S c)). + intro. left. apply not_all_ex_not in H2. destruct H2. apply imply_to_and in H2. destruct H2. apply (ord_trans ord) with x0. * pose proof (H0 x0 H2 x H1). tauto. * now apply (proj2_sig (chain_sup S c)). - pose proof (proj2_sig (inflation x)). destruct H0, H1. remember (proj1_sig (inflation x)) as x'. assert (forall y:T, In tower y -> R y x \/ R x' y). + intros. induction H3. * case (classic (forall x0:T, In S x0 -> R x0 x)); trivial. left. now apply (proj2_sig (chain_sup S c)). right. apply not_all_ex_not in H5. destruct H5. apply imply_to_and in H5. destruct H5. apply (ord_trans ord) with x0. ** pose proof (H4 x0). tauto. ** now apply (proj2_sig (chain_sup S c)). * assert (In tower x'). rewrite Heqx'. now apply inflation_intro. destruct IHtower0. ** assert (In tower (proj1_sig (inflation x0))) by now apply inflation_intro. case (IHtower (proj1_sig (inflation x0)) H6); [ now left | ]. intro. pose proof (proj2_sig (inflation x0)). simpl in H8. assert (x = x0 \/ x = proj1_sig (inflation x0)) by now apply H8. case H9. *** right. rewrite Heqx', H10. apply (ord_refl ord). *** left. rewrite H10. apply (ord_refl ord). ** right. now apply (ord_trans ord) with x0, (proj2_sig (inflation x0)). + intros. case (H3 x0 H4). * left. now apply (ord_trans ord) with x. * now right. Qed.
imports: Classical ClassicalChoice Relation_Definitions Relation_Definitions_Implicit Ensembles EnsemblesImplicit ProofIrrelevance InverseImage EnsemblesSpec Quotients