let rec Acc_ind (A: Type[0]) (R: (A \to (A \to Prop))) (P: (A \to 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
let rec Acc_ind (A: Type[0]) (R: (A \to (A \to Prop))) (P: (A \to 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