- \lambda (c: C).(C_ind (\lambda (c0: C).(csubv c0 c0)) (\lambda (n:
-nat).(csubv_sort n)) (\lambda (c0: C).(\lambda (H: (csubv c0 c0)).(\lambda
-(k: K).(K_ind (\lambda (k0: K).(\forall (t: T).(csubv (CHead c0 k0 t) (CHead
-c0 k0 t)))) (\lambda (b: B).(\lambda (t: T).(csubv_bind_same c0 c0 H b t t)))
-(\lambda (f: F).(\lambda (t: T).(csubv_flat c0 c0 H f f t t))) k)))) c).
-(* COMMENTS
-Initial nodes: 93
-END *)
+ \lambda (c: C).(let TMP_1 \def (\lambda (c0: C).(csubv c0 c0)) in (let TMP_2
+\def (\lambda (n: nat).(csubv_sort n)) in (let TMP_8 \def (\lambda (c0:
+C).(\lambda (H: (csubv c0 c0)).(\lambda (k: K).(let TMP_5 \def (\lambda (k0:
+K).(\forall (t: T).(let TMP_3 \def (CHead c0 k0 t) in (let TMP_4 \def (CHead
+c0 k0 t) in (csubv TMP_3 TMP_4))))) in (let TMP_6 \def (\lambda (b:
+B).(\lambda (t: T).(csubv_bind_same c0 c0 H b t t))) in (let TMP_7 \def
+(\lambda (f: F).(\lambda (t: T).(csubv_flat c0 c0 H f f t t))) in (K_ind
+TMP_5 TMP_6 TMP_7 k))))))) in (C_ind TMP_1 TMP_2 TMP_8 c)))).