proposition: Lemma partial_WO_preord : preorder partial_WO_ord.
proof: Proof. constructor. unfold reflexive. intro. destruct x. constructor; simpl. auto with sets. split. trivial. trivial. auto. unfold transitive. destruct x. destruct y. destruct z. intros. destruct H. destruct H0. simpl in pwo_S_incl0; simpl in pwo_restriction0; simpl in pwo_downward_closed0; simpl in pwo_S_incl1; simpl in pwo_restriction1; simpl in pwo_downward_closed1. 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: Relation_Definitions Relation_Definitions_Implicit Classical_Wf Description FunctionalExtensionality Classical ZornsLemma ProofIrrelevance EnsemblesSpec