-(H1: (eq nat (fweight c0 t0) n0)).(let H2 \def (eq_ind_r nat n0 (\lambda (n:
-nat).(\forall (m: nat).((lt m n) \to (\forall (c: C).(\forall (t: T).((eq nat
-(fweight c t) m) \to (P c t))))))) H0 (fweight c0 t0) H1) in (H c0 t0
+(H1: (eq nat (fweight c0 t0) n0)).(let H2 \def (eq_ind_r nat n0 (\lambda (n1:
+nat).(\forall (m: nat).((lt m n1) \to (\forall (c1: C).(\forall (t1: T).((eq
+nat (fweight c1 t1) m) \to (P c1 t1))))))) H0 (fweight c0 t0) H1) in (H c0 t0