(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/wf3/ty3.ma".
+include "Basic-1/wf3/ty3.ma".
-include "LambdaDelta-1/app/defs.ma".
+include "Basic-1/app/defs.ma".
theorem wf3_mono:
\forall (g: G).(\forall (c: C).(\forall (c1: C).((wf3 g c c1) \to (\forall
T).(\lambda (f: F).(\lambda (c0: C).(\lambda (H2: (wf3 g (CHead c2 (Flat f)
u) c0)).(let H_y \def (wf3_gen_flat1 g c2 c0 u f H2) in (H1 c0 H_y))))))))))
c c1 H)))).
+(* COMMENTS
+Initial nodes: 1555
+END *)
theorem wf3_total:
\forall (g: G).(\forall (c1: C).(ex C (\lambda (c2: C).(wf3 g c1 c2))))
(CHead x (Bind Void) (TSort O)) (wf3_void g c x H1 t H3 b))) H2)))) (\lambda
(f: F).(ex_intro C (\lambda (c2: C).(wf3 g (CHead c (Flat f) t) c2)) x
(wf3_flat g c x H1 t f))) k))) H0)))))) c1)).
+(* COMMENTS
+Initial nodes: 435
+END *)
theorem ty3_shift1:
\forall (g: G).(\forall (c: C).((wf3 g c c) \to (\forall (t1: T).(\forall
(Bind x) H9) in (False_ind (ty3 g (CSort (cbk c1)) (app1 c1 (THead (Flat f) u
t1)) (app1 c1 (THead (Flat f) u t2))) H10)))) H8)))))))))))))))) y c H0)))
H))).
+(* COMMENTS
+Initial nodes: 1677
+END *)
theorem wf3_idem:
\forall (g: G).(\forall (c1: C).(\forall (c2: C).((wf3 g c1 c2) \to (wf3 g
c4 H1 (TSort O) (TSort (next g O)) (ty3_sort g c4 O) Void)))))))) (\lambda
(c3: C).(\lambda (c4: C).(\lambda (_: (wf3 g c3 c4)).(\lambda (H1: (wf3 g c4
c4)).(\lambda (_: T).(\lambda (_: F).H1)))))) c1 c2 H)))).
+(* COMMENTS
+Initial nodes: 207
+END *)
theorem wf3_ty3:
\forall (g: G).(\forall (c1: C).(\forall (t: T).(\forall (u: T).((ty3 g c1 t
(\lambda (c2: C).(ty3 g c2 t u))) (\lambda (x: C).(\lambda (H1: (wf3 g c1
x)).(ex_intro2 C (\lambda (c2: C).(wf3 g c1 c2)) (\lambda (c2: C).(ty3 g c2 t
u)) x H1 (wf3_ty3_conf g c1 t u H x H1)))) H0))))))).
+(* COMMENTS
+Initial nodes: 123
+END *)