Prop)) (f: (\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
Prop)) (f: (\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