-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
-\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)))))].
+implied rec lemma 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 \def match a0 with [(Acc_intro x a1) \Rightarrow (f x a1 (\lambda
+(y: A).(\lambda (r0: (R y x)).((Acc_ind A R P f) y (a1 y r0)))))].