-nat).(\lambda (d: nat).(eq_ind_r T (THead k (lift i d v) (lift i (s k d) t0))
-(\lambda (t1: T).(cnt t1)) (cnt_head (lift i (s k d) t0) (H1 i (s k d)) k
-(lift i d v)) (lift i d (THead k v t0)) (lift_head k v t0 i d))))))))) t H)).
-(* COMMENTS
-Initial nodes: 191
-END *)
+nat).(\lambda (d: nat).(let TMP_10 \def (lift i d v) in (let TMP_11 \def (s k
+d) in (let TMP_12 \def (lift i TMP_11 t0) in (let TMP_13 \def (THead k TMP_10
+TMP_12) in (let TMP_14 \def (\lambda (t1: T).(cnt t1)) in (let TMP_15 \def (s
+k d) in (let TMP_16 \def (lift i TMP_15 t0) in (let TMP_17 \def (s k d) in
+(let TMP_18 \def (H1 i TMP_17) in (let TMP_19 \def (lift i d v) in (let
+TMP_20 \def (cnt_head TMP_16 TMP_18 k TMP_19) in (let TMP_21 \def (THead k v
+t0) in (let TMP_22 \def (lift i d TMP_21) in (let TMP_23 \def (lift_head k v
+t0 i d) in (eq_ind_r T TMP_13 TMP_14 TMP_20 TMP_22
+TMP_23)))))))))))))))))))))) in (cnt_ind TMP_2 TMP_9 TMP_24 t H))))).