(\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:
(\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: