Library Coq.Wellfounded.Inclusion
Author: Bruno Barras
Require
Import
Relation_Definitions
.
Section
WfInclusion
.
Variable
A
:
Type
.
Variables
R1
R2
:
A
->
A
->
Prop
.
Lemma
Acc_incl
:
inclusion
A
R1
R2
->
forall
z
:
A
,
Acc
R2
z
->
Acc
R1
z
.
Hint Resolve
Acc_incl
.
Theorem
wf_incl
:
inclusion
A
R1
R2
->
well_founded
R2
->
well_founded
R1
.
End
WfInclusion
.