proposition: Lemma wf_incl_transparent : forall (A : Type) (R1 R2 : A -> A -> Prop), Relation_Definitions.inclusion A R1 R2 -> well_founded R2 -> well_founded R1.
proof: Proof. intros A R1 R2 H H0 a; induction (H0 a). split; auto. Defined.