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