\forall (t: T).(iso t t)
\def
\lambda (t: T).(T_ind (\lambda (t0: T).(iso t0 t0)) (\lambda (n:
nat).(iso_sort n n)) (\lambda (n: nat).(iso_lref n n)) (\lambda (k:
K).(\lambda (t0: T).(\lambda (_: (iso t0 t0)).(\lambda (t1: T).(\lambda (_:
(iso t1 t1)).(iso_head t0 t0 t1 t1 k)))))) t).
\forall (t: T).(iso t t)
\def
\lambda (t: T).(T_ind (\lambda (t0: T).(iso t0 t0)) (\lambda (n:
nat).(iso_sort n n)) (\lambda (n: nat).(iso_lref n n)) (\lambda (k:
K).(\lambda (t0: T).(\lambda (_: (iso t0 t0)).(\lambda (t1: T).(\lambda (_:
(iso t1 t1)).(iso_head t0 t0 t1 t1 k)))))) t).
(\lambda (x0: T).(\lambda (x1: T).(\lambda (H2: (eq T t5 (THead k x0
x1))).(eq_ind_r T (THead k x0 x1) (\lambda (t: T).(iso (THead k v1 t3) t))
(iso_head v1 x0 t3 x1 k) t5 H2)))) H1)))))))))) t1 t2 H))).
(\lambda (x0: T).(\lambda (x1: T).(\lambda (H2: (eq T t5 (THead k x0
x1))).(eq_ind_r T (THead k x0 x1) (\lambda (t: T).(iso (THead k v1 t3) t))
(iso_head v1 x0 t3 x1 k) t5 H2)))) H1)))))))))) t1 t2 H))).