proposition: Lemma ZL': False.
proof: Proof. pose proof (proj2_sig (chain_sup tower tower_is_chain)). simpl in H. remember (proj1_sig (chain_sup tower tower_is_chain)) as x0. assert (In tower x0). { rewrite Heqx0. constructor 1. auto with sets. } pose (x' := proj1_sig (inflation x0)). assert (In tower x') by now constructor 2. pose proof (proj2_sig (inflation x0)). destruct H2, H3. contradict H3. apply (ord_antisym ord); trivial. destruct H. now apply H. Qed.
imports: Coq(ClassicalChoice) ZornsLemma(Relation_Definitions_Implicit) ZornsLemma(EnsemblesImplicit) Coq(ProofIrrelevance) Coq(PropExtensionalityFacts) ZornsLemma(InverseImage) ZornsLemma(Quotients)