inductive arity (g: G): C \to (T \to (A \to Prop)) \def
| arity_sort: \forall (c: C).(\forall (n: nat).(arity g c (TSort n) (ASort O
inductive arity (g: G): C \to (T \to (A \to Prop)) \def
| arity_sort: \forall (c: C).(\forall (n: nat).(arity g c (TSort n) (ASort O