-let rec sty1_ind (g: G) (c: C) (t1: T) (P: (T \to Prop)) (f: (\forall (t2:
-T).((sty0 g c t1 t2) \to (P t2)))) (f0: (\forall (t: T).((sty1 g c t1 t) \to
-((P t) \to (\forall (t2: T).((sty0 g c t t2) \to (P t2))))))) (t: T) (s0:
+implied let rec sty1_ind (g: G) (c: C) (t1: T) (P: (T \to Prop)) (f: (\forall
+(t2: T).((sty0 g c t1 t2) \to (P t2)))) (f0: (\forall (t: T).((sty1 g c t1 t)
+\to ((P t) \to (\forall (t2: T).((sty0 g c t t2) \to (P t2))))))) (t: T) (s0: