# Inclusion preserves well-founded

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

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

## Solution

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