(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/cnt/defs.ma".
+include "Basic-1/cnt/defs.ma".
-include "LambdaDelta-1/lift/fwd.ma".
+include "Basic-1/lift/fwd.ma".
theorem cnt_lift:
\forall (t: T).((cnt t) \to (\forall (i: nat).(\forall (d: nat).(cnt (lift i
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 *)