(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/wf3/clear.ma".
+include "Basic-1/wf3/clear.ma".
-include "LambdaDelta-1/ty3/dec.ma".
+include "Basic-1/ty3/dec.ma".
theorem wf3_getl_conf:
\forall (b: B).(\forall (i: nat).(\forall (c1: C).(\forall (d1: C).(\forall
(CHead d1 (Bind b) v))).(let H_y \def (wf3_gen_flat1 g c c2 t f H4) in (H0 d1
v H5 g c2 H_y w H3))))) k H2 (getl_gen_S k c (CHead d1 (Bind b) v) t n
H1)))))))))))))) c1)))) i)).
+(* COMMENTS
+Initial nodes: 2531
+END *)
theorem getl_wf3_trans:
\forall (i: nat).(\forall (c1: C).(\forall (d1: C).((getl i c1 d1) \to
n) x d2)).(ex_intro2 C (\lambda (c2: C).(wf3 g (CHead c (Flat f) t) c2))
(\lambda (c2: C).(getl (S n) c2 d2)) x (wf3_flat g c x H5 t f) H6)))) H4)))))
k (getl_gen_S k c d1 t n H1))))))))))) c1)))) i).
+(* COMMENTS
+Initial nodes: 1139
+END *)