-let rec sty0_ind (g: G) (P: (C \to (T \to (T \to Prop)))) (f: (\forall (c:
-C).(\forall (n: nat).(P c (TSort n) (TSort (next g n)))))) (f0: (\forall (c:
-C).(\forall (d: C).(\forall (v: T).(\forall (i: nat).((getl i c (CHead d
-(Bind Abbr) v)) \to (\forall (w: T).((sty0 g d v w) \to ((P d v w) \to (P c
-(TLRef i) (lift (S i) O w))))))))))) (f1: (\forall (c: C).(\forall (d:
-C).(\forall (v: T).(\forall (i: nat).((getl i c (CHead d (Bind Abst) v)) \to
-(\forall (w: T).((sty0 g d v w) \to ((P d v w) \to (P c (TLRef i) (lift (S i)
-O v))))))))))) (f2: (\forall (b: B).(\forall (c: C).(\forall (v: T).(\forall
-(t1: T).(\forall (t2: T).((sty0 g (CHead c (Bind b) v) t1 t2) \to ((P (CHead
-c (Bind b) v) t1 t2) \to (P c (THead (Bind b) v t1) (THead (Bind b) v
-t2)))))))))) (f3: (\forall (c: C).(\forall (v: T).(\forall (t1: T).(\forall
-(t2: T).((sty0 g c t1 t2) \to ((P c t1 t2) \to (P c (THead (Flat Appl) v t1)
-(THead (Flat Appl) v t2))))))))) (f4: (\forall (c: C).(\forall (v1:
-T).(\forall (v2: T).((sty0 g c v1 v2) \to ((P c v1 v2) \to (\forall (t1:
+implied rec lemma sty0_ind (g: G) (P: (C \to (T \to (T \to Prop)))) (f:
+(\forall (c: C).(\forall (n: nat).(P c (TSort n) (TSort (next g n)))))) (f0:
+(\forall (c: C).(\forall (d: C).(\forall (v: T).(\forall (i: nat).((getl i c
+(CHead d (Bind Abbr) v)) \to (\forall (w: T).((sty0 g d v w) \to ((P d v w)
+\to (P c (TLRef i) (lift (S i) O w))))))))))) (f1: (\forall (c: C).(\forall
+(d: C).(\forall (v: T).(\forall (i: nat).((getl i c (CHead d (Bind Abst) v))
+\to (\forall (w: T).((sty0 g d v w) \to ((P d v w) \to (P c (TLRef i) (lift
+(S i) O v))))))))))) (f2: (\forall (b: B).(\forall (c: C).(\forall (v:
+T).(\forall (t1: T).(\forall (t2: T).((sty0 g (CHead c (Bind b) v) t1 t2) \to
+((P (CHead c (Bind b) v) t1 t2) \to (P c (THead (Bind b) v t1) (THead (Bind
+b) v t2)))))))))) (f3: (\forall (c: C).(\forall (v: T).(\forall (t1:
+T).(\forall (t2: T).((sty0 g c t1 t2) \to ((P c t1 t2) \to (P c (THead (Flat
+Appl) v t1) (THead (Flat Appl) v t2))))))))) (f4: (\forall (c: C).(\forall
+(v1: T).(\forall (v2: T).((sty0 g c v1 v2) \to ((P c v1 v2) \to (\forall (t1: