-let rec arity_ind (g: G) (P: (C \to (T \to (A \to Prop)))) (f: (\forall (c:
-C).(\forall (n: nat).(P c (TSort n) (ASort O n))))) (f0: (\forall (c:
-C).(\forall (d: C).(\forall (u: T).(\forall (i: nat).((getl i c (CHead d
-(Bind Abbr) u)) \to (\forall (a: A).((arity g d u a) \to ((P d u a) \to (P c
-(TLRef i) a)))))))))) (f1: (\forall (c: C).(\forall (d: C).(\forall (u:
-T).(\forall (i: nat).((getl i c (CHead d (Bind Abst) u)) \to (\forall (a:
+implied rec lemma arity_ind (g: G) (P: (C \to (T \to (A \to Prop)))) (f:
+(\forall (c: C).(\forall (n: nat).(P c (TSort n) (ASort O n))))) (f0:
+(\forall (c: C).(\forall (d: C).(\forall (u: T).(\forall (i: nat).((getl i c
+(CHead d (Bind Abbr) u)) \to (\forall (a: A).((arity g d u a) \to ((P d u a)
+\to (P c (TLRef i) a)))))))))) (f1: (\forall (c: C).(\forall (d: C).(\forall
+(u: T).(\forall (i: nat).((getl i c (CHead d (Bind Abst) u)) \to (\forall (a: