Library Stdlib.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.
#[local]
Hint Resolve Acc_incl : core.
Theorem wf_incl : inclusion A R1 R2 -> well_founded R2 -> well_founded R1.
End WfInclusion.