Inclusion preserves well-founded

Prove the following theorem (the constant inclusion is defined in module Relations).

  forall (A:Set) (R S:A->A->Prop),
    inclusion A R S -> well_founded A S -> well_founded A R.


The solution to this exercise is given in the Coq libraries

Going home
Yves Bertot
Last modified: Thu May 15 10:16:48 MEST 2003