-implied let rec ty3_ind (g: G) (P: (C \to (T \to (T \to Prop)))) (f: (\forall
-(c: C).(\forall (t2: T).(\forall (t: T).((ty3 g c t2 t) \to ((P c t2 t) \to
-(\forall (u: T).(\forall (t1: T).((ty3 g c u t1) \to ((P c u t1) \to ((pc3 c
-t1 t2) \to (P c u t2)))))))))))) (f0: (\forall (c: C).(\forall (m: nat).(P c
-(TSort m) (TSort (next g m)))))) (f1: (\forall (n: nat).(\forall (c:
-C).(\forall (d: C).(\forall (u: T).((getl n c (CHead d (Bind Abbr) u)) \to
-(\forall (t: T).((ty3 g d u t) \to ((P d u t) \to (P c (TLRef n) (lift (S n)
-O t))))))))))) (f2: (\forall (n: nat).(\forall (c: C).(\forall (d:
+implied rec lemma ty3_ind (g: G) (P: (C \to (T \to (T \to Prop)))) (f:
+(\forall (c: C).(\forall (t2: T).(\forall (t: T).((ty3 g c t2 t) \to ((P c t2
+t) \to (\forall (u: T).(\forall (t1: T).((ty3 g c u t1) \to ((P c u t1) \to
+((pc3 c t1 t2) \to (P c u t2)))))))))))) (f0: (\forall (c: C).(\forall (m:
+nat).(P c (TSort m) (TSort (next g m)))))) (f1: (\forall (n: nat).(\forall
+(c: C).(\forall (d: C).(\forall (u: T).((getl n c (CHead d (Bind Abbr) u))
+\to (\forall (t: T).((ty3 g d u t) \to ((P d u t) \to (P c (TLRef n) (lift (S
+n) O t))))))))))) (f2: (\forall (n: nat).(\forall (c: C).(\forall (d: