proposition: Theorem AccElim3 : forall A B C:Type, forall (RA:A->A->Prop) (RB:B->B->Prop) (RC:C->C->Prop), forall (P : A -> B -> C -> Prop), (forall x y z, (forall (t : A), RA t x -> forall y' z', Acc RB y' -> Acc RC z' -> P t y' z') -> (forall (t : B), RB t y -> forall z', Acc RC z' -> P x t z') -> (forall (t : C), RC t z -> P x y t) -> P x y z) -> forall x y z, Acc RA x -> Acc RB y -> Acc RC z -> P x y z.
proof: 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.