Section Prop_induction.

 Variable A : Set.
 Variable R : A → A → Prop.
 Hypothesis W : well_founded R.
 Hint Resolve W: arith.

 Lemma Prop_wfi :
  ∀ P : A → Prop,
  (∀ x : A, (∀ y : A, R y x → P y) → P x) → ∀ a : A, P a.
 Proof.
  intros; apply (Acc_ind (R:=R) P); auto.
 Qed.

End Prop_induction.

Definition coarser (A : Set) (R S : A → A → Prop) :=
  ∀ x y : A, R x y → S x y.

Lemma wf_coarser :
 ∀ (A : Set) (R S : A → A → Prop),
 coarser A R S → well_founded S → well_founded R.
Proof.
 unfold well_founded in |- *; intros A R S H H0 a.
 apply Acc_intro; intros y H1.
 pattern y in |- *; apply Prop_wfi with A S.
 exact H0.
 intros; apply Acc_intro; auto.
Qed.