proposition: Lemma union_good (F: order → Prop) (F_chain: ∀ o o', F o → F o' → o ≼ o' ∨ o' ≼ o): ordered_subset (union_S F) (union_R F).
proof: Proof. unfold union_S, union_R. split. 2:split. - solve_proper. - intros x [o [_ [ ]%irreflexivity]]. - intros x y z [o [ino sto]] [o' [ino' sto']]. destruct (F_chain _ _ ino ino') as [case|case]. + exists o'; split; trivial; transitivity y; trivial. apply continuation_subrelation in case. apply case, sto. + exists o; split; trivial; transitivity y; trivial. apply continuation_subrelation in case. apply case, sto'. - intro a. constructor. intros b [o [ino rel]]. destruct (o.good) as [sproper rstrict rwf rproper rcorrect rcomplete]. apply rcorrect in rel. destruct rel as [inb _]; clear a. induction b as [a IH] using (well_founded_ind rwf). constructor. intros b [o' [ino' rel]]. destruct (F_chain _ _ ino ino') as [case|case]. + destruct case as [sub closed coincides]. rewrite <- coincides in rel; auto. * apply IH; trivial. apply rcorrect in rel; tauto. * eapply closed; eauto. destruct (o'.good) as [_ _ _ _ correct _]. apply correct in rel; tauto. + apply IH. * apply continuation_subrelation in case. apply case, rel. * apply continuation_subrelation in case. apply case in rel. destruct (o.good) as [_ _ _ _ correct _]. apply correct in rel; tauto. - solve_proper. - intros x y [o [ino relo]]. destruct (o.good) as [_ _ _ _ correct _]. apply correct in relo. destruct relo; split; eauto. - intros x y [o [ino relo]] [o' [ino' relo']]. destruct (F_chain o o' ino ino') as [case|case]. + destruct (case) as [S_sub _ _]. apply S_sub in relo. destruct (o'.good) as [_ _ _ _ _ complete]. destruct (complete x y) as [?|[?|?]]; eauto. + destruct (case) as [S_sub _ _]. apply S_sub in relo'. destruct (o.good) as [_ _ _ _ _ complete]. destruct (complete x y) as [?|[?|?]]; eauto. Qed.
imports: Coq(Relations Equivalence Morphisms Utf8) Coq(ChoiceFacts ClassicalFacts) Coq.Program(Basics) Coq.Logic(SetoidChoice)