Library Stdlib.Wellfounded.Union
Author: Bruno Barras
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.