Section restricted_recursion.

 Variables (A:Type)(P:A→Prop)(R:A→A→Prop).

 Definition restrict (a b:A):Prop :=
   P a ∧ R a b ∧ P b.

 Definition well_founded_P := ∀ (a:A), P a → Acc restrict a.

 Definition P_well_founded_induction_type :
       well_founded_P →
       ∀ X : A → Type,
       (∀ x : A, P x → (∀ y : A,P y→ R y x → X y) → X x) →
       ∀ a : A, P a → X a.
  intros W X H a.
  pattern a; eapply well_founded_induction_type with (R:=restrict).
  unfold well_founded.
  split.
  unfold well_founded_P in W.
  intros; apply W.
 case H0.
 auto.
 intros; apply H.
 auto.
 intros; apply X0.
 unfold restrict; auto.
 auto.
Defined.

End restricted_recursion.

Theorem AccElim3 :
∀ A B C:Type,
 ∀ (RA:A→A→Prop)
        (RB:B→B→Prop)
        (RC:C→C→Prop),
 ∀ (P : A → B → C → Prop),
 (∀ x y z,
    (∀ (t : A), RA t x →
                     ∀ y' z', Acc RB y' → Acc RC z' →
                                   P t y' z') →
    (∀ (t : B), RB t y →
                     ∀ z', Acc RC z' → P x t z') →
    (∀ (t : C), RC t z → P x y t) →
    P x y z) →
  ∀ x y z, Acc RA x → Acc RB y → Acc RC z → P x y z.
Proof.
 intros A B C RA RB RC P H x y z Ax; generalize y z; clear y z.
 elim Ax; clear Ax x; intros x _ Hrecx y z Ay; generalize z; clear z.
 elim Ay; clear Ay y;
 intros y _ Hrecy z Az; elim Az; clear Az z; auto.
Qed.

Theorem accElim3:
 ∀ (A B C:Set)(RA : A → A →Prop) (RB : B→ B→ Prop)
                   (RC : C → C → Prop)(P : A → B → C → Prop),
 (∀ x y z ,
  (∀ (t : A), RA t x → P t y z) →
  (∀ (t : B), RB t y → P x t z) →
  (∀ (t : C), RC t z → P x y t) → P x y z) →
 ∀ x y z, Acc RA x → Acc RB y → Acc RC z → P x y z.

intros A B C RA RB RC P H x y z Ax Ay Az.
 generalize Ax Ay Az.
 pattern x, y, z;
 eapply AccElim3 with (RA:=RA)(RB:=RB)(RC:=RC) ;eauto.
 intros; apply H.

 intros;apply H0; auto.
 eapply Acc_inv;eauto.
 intros;apply H1; auto.
 eapply Acc_inv;eauto.
 intros;apply H2; auto.
  eapply Acc_inv;eauto.
Qed.