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.
The solution to this exercise is given in the Coq libraries