-let rec tys3_ind (g: G) (c: C) (P: (TList \to (T \to Prop))) (f: (\forall (u:
-T).(\forall (u0: T).((ty3 g c u u0) \to (P TNil u))))) (f0: (\forall (t:
-T).(\forall (u: T).((ty3 g c t u) \to (\forall (ts: TList).((tys3 g c ts u)
-\to ((P ts u) \to (P (TCons t ts) u)))))))) (t: TList) (t0: T) (t1: tys3 g c
-t t0) on t1: P t t0 \def match t1 with [(tys3_nil u u0 t2) \Rightarrow (f u
-u0 t2) | (tys3_cons t2 u t3 ts t4) \Rightarrow (f0 t2 u t3 ts t4 ((tys3_ind g
-c P f f0) ts u t4))].
+implied let rec tys3_ind (g: G) (c: C) (P: (TList \to (T \to Prop))) (f:
+(\forall (u: T).(\forall (u0: T).((ty3 g c u u0) \to (P TNil u))))) (f0:
+(\forall (t: T).(\forall (u: T).((ty3 g c t u) \to (\forall (ts:
+TList).((tys3 g c ts u) \to ((P ts u) \to (P (TCons t ts) u)))))))) (t:
+TList) (t0: T) (t1: tys3 g c t t0) on t1: P t t0 \def match t1 with
+[(tys3_nil u u0 t2) \Rightarrow (f u u0 t2) | (tys3_cons t2 u t3 ts t4)
+\Rightarrow (f0 t2 u t3 ts t4 ((tys3_ind g c P f f0) ts u t4))].