Library Coq.Wellfounded.Union

Require Import Relation_Operators.
Require Import Relation_Definitions.
Require Import Transitive_Closure.

Section WfUnion.
  Variable A : Type.
  Variables R1 R2 : relation A.

  Notation Union := (union A R1 R2).

  Remark strip_commut :
    commut A R1 R2 ->
    forall x y:A,
      clos_trans A R1 y x ->
      forall z:A, R2 z y -> exists2 y´ : A, R2 y´ x & clos_trans A R1 z y´.

  Lemma Acc_union :
    commut A R1 R2 ->
    (forall x:A, Acc R2 x -> Acc R1 x) -> forall a:A, Acc R2 a -> Acc Union a.

  Theorem wf_union :
    commut A R1 R2 -> well_founded R1 -> well_founded R2 -> well_founded Union.

End WfUnion.