proposition: Lemma extend_strictly_partial_WO_correct: forall (WO:partial_WO) (x:T) (ni:~ In (pwo_S WO) x), partial_WO_ord WO (extend_strictly_partial_WO WO x ni).
proof: Proof. intros. constructor. unfold extend_strictly_partial_WO; simpl. constructor 1. assumption. intros. unfold extend_strictly_partial_WO; simpl. split. tauto. intro. case H1. trivial. intro. destruct H2. contradict ni. rewrite <- H3. assumption. unfold extend_strictly_partial_WO; simpl. intros. case H1. intro. pose proof (pwo_R_lives_on_S WO x0 y). tauto. intro. tauto. Qed.
imports: Relation_Definitions Relation_Definitions_Implicit Classical_Wf Description FunctionalExtensionality Classical ZornsLemma ProofIrrelevance EnsemblesSpec