Library Coq.Wellfounded.Inclusion

Author: Bruno Barras




Require Import Relation_Definitions.




Section WfInclusion.

  Variable A : Set.

  Variables R1 R2 : A -> A -> Prop.




  Lemma Acc_incl : inclusion A R1 R2 -> forall z:A, Acc R2 z -> Acc R1 z.

  Proof.

    induction 2.

    apply Acc_intro; auto with sets.

  Qed.




  Hint Resolve Acc_incl.




  Theorem wf_incl : inclusion A R1 R2 -> well_founded R2 -> well_founded R1.

  Proof.

    unfold well_founded in |- *; auto with sets.

  Qed.




End WfInclusion.