\forall (P: ((A \to Prop))).(((\forall (n: nat).((\lambda (P0: ((A \to
Prop))).(\lambda (n0: nat).(\forall (a: A).((eq nat (lweight a) n0) \to (P0
a))))) P n))) \to (\forall (a: A).(P a)))
\forall (P: ((A \to Prop))).(((\forall (n: nat).((\lambda (P0: ((A \to
Prop))).(\lambda (n0: nat).(\forall (a: A).((eq nat (lweight a) n0) \to (P0
a))))) P n))) \to (\forall (a: A).(P a)))