proposition: Lemma partial_WO_preord : preorder partial_WO_ord.
proof: Proof. constructor. - unfold reflexive. intro. destruct x. constructor; simpl. + auto with sets. + split; trivial. + auto. - unfold transitive. destruct x. destruct y. destruct z. intros. destruct H. destruct H0. simpl in *. constructor; simpl. + auto with sets. + intros. apply iff_trans with (pwo_R1 x y). * apply pwo_restriction0; auto with sets. * apply pwo_restriction1; auto with sets. + intros. apply pwo_downward_closed0 with y; trivial. * apply pwo_downward_closed1 with y; trivial. auto with sets. * apply <- (pwo_restriction1 x y); trivial. -- auto with sets. -- apply pwo_downward_closed1 with y; trivial. auto with sets. Qed.
imports: Coq(Classical Description FunctionalExtensionality ProofIrrelevance) ZornsLemma(Classical_Wf EnsemblesSpec Relation_Definitions_Implicit ZornsLemma)