(P: ((C \to (T \to Prop)))).(\lambda (H: ((\forall (n: nat).(\forall (c:
C).(\forall (t: T).((eq nat (fweight c t) n) \to (P c t))))))).(\lambda (c:
C).(\lambda (t: T).(H (fweight c t) c t (refl_equal nat (fweight c t))))))).
(P: ((C \to (T \to Prop)))).(\lambda (H: ((\forall (n: nat).(\forall (c:
C).(\forall (t: T).((eq nat (fweight c t) n) \to (P c t))))))).(\lambda (c:
C).(\lambda (t: T).(H (fweight c t) c t (refl_equal nat (fweight c t))))))).