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