(\forall (x: A).(((\forall (y: A).((R y x) \to (Acc A R y)))) \to (((\forall
(y: A).((R y x) \to (P y)))) \to (P x))))) (a: A) (a0: Acc A R a) on a0: P a
\def match a0 with [(Acc_intro x a1) \Rightarrow (f x a1 (\lambda (y:
-A).(\lambda (r: (R y x)).((Acc_ind A R P f) y (a1 y r)))))].
+A).(\lambda (r0: (R y x)).((Acc_ind A R P f) y (a1 y r0)))))].