\forall (P: ((T \to Prop))).(((\forall (n: nat).((\lambda (P0: ((T \to
Prop))).(\lambda (n0: nat).(\forall (t: T).((eq nat (weight t) n0) \to (P0
t))))) P n))) \to (\forall (t: T).(P t)))
\forall (P: ((T \to Prop))).(((\forall (n: nat).((\lambda (P0: ((T \to
Prop))).(\lambda (n0: nat).(\forall (t: T).((eq nat (weight t) n0) \to (P0
t))))) P n))) \to (\forall (t: T).(P t)))