(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/clen/defs.ma".
+include "Basic-1/clen/defs.ma".
-include "LambdaDelta-1/getl/props.ma".
+include "Basic-1/getl/props.ma".
theorem getl_ctail_clen:
\forall (b: B).(\forall (t: T).(\forall (c: C).(ex nat (\lambda (n:
F).(ex_intro nat (\lambda (n: nat).(getl (clen c0) (CHead (CTail (Bind b) t
c0) (Flat f) t0) (CHead (CSort n) (Bind b) t))) x (getl_flat (CTail (Bind b)
t c0) (CHead (CSort x) (Bind b) t) (clen c0) H1 f t0))) k))) H0)))))) c))).
+(* COMMENTS
+Initial nodes: 459
+END *)
theorem getl_gen_tail:
\forall (k: K).(\forall (b: B).(\forall (u1: T).(\forall (u2: T).(\forall
(Bind b)) (refl_equal T u1) (refl_equal C (CSort x0)))) (s k0 (r k0 n)) (s_r
k0 n)) (clen c) H4) k H5))) u2 H6))) c2 H7)))))))) H3)) H2)))))) i))))))
c1)))))).
+(* COMMENTS
+Initial nodes: 7489
+END *)