- \lambda (k: K).(\lambda (vs: TList).(TList_ind (\lambda (t: TList).(\forall
-(v: T).(\forall (t0: T).(eq T (THeads k (TApp t v) t0) (THeads k t (THead k v
-t0)))))) (\lambda (v: T).(\lambda (t: T).(refl_equal T (THead k v t))))
-(\lambda (t: T).(\lambda (t0: TList).(\lambda (H: ((\forall (v: T).(\forall
-(t1: T).(eq T (THeads k (TApp t0 v) t1) (THeads k t0 (THead k v
-t1))))))).(\lambda (v: T).(\lambda (t1: T).(eq_ind_r T (THeads k t0 (THead k
-v t1)) (\lambda (t2: T).(eq T (THead k t t2) (THead k t (THeads k t0 (THead k
-v t1))))) (refl_equal T (THead k t (THeads k t0 (THead k v t1)))) (THeads k
-(TApp t0 v) t1) (H v t1))))))) vs)).
+ \lambda (k: K).(\lambda (v: T).(\lambda (t: T).(\lambda (vs:
+TList).(TList_ind (\lambda (t0: TList).(eq T (THeads k (TApp t0 v) t) (THeads
+k t0 (THead k v t)))) (refl_equal T (THead k v t)) (\lambda (t0: T).(\lambda
+(t1: TList).(\lambda (H: (eq T (THeads k (TApp t1 v) t) (THeads k t1 (THead k
+v t)))).(eq_ind T (THeads k (TApp t1 v) t) (\lambda (t2: T).(eq T (THead k t0
+(THeads k (TApp t1 v) t)) (THead k t0 t2))) (refl_equal T (THead k t0 (THeads
+k (TApp t1 v) t))) (THeads k t1 (THead k v t)) H)))) vs)))).