(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/wf3/defs.ma".
+include "Basic-1/wf3/defs.ma".
theorem wf3_gen_sort1:
\forall (g: G).(\forall (x: C).(\forall (m: nat).((wf3 g (CSort m) x) \to
C).(match ee in C return (\lambda (_: C).Prop) with [(CSort _) \Rightarrow
False | (CHead _ _ _) \Rightarrow True])) I (CSort m) H3) in (False_ind (eq C
c2 (CHead c1 (Flat f) u)) H4))))))))) y x H0))) H)))).
+(* COMMENTS
+Initial nodes: 523
+END *)
theorem wf3_gen_bind1:
\forall (g: G).(\forall (c1: C).(\forall (x: C).(\forall (v: T).(\forall (b:
g c1 v w)))) (ex3 C (\lambda (c3: C).(eq C c2 (CHead c3 (Bind Void) (TSort
O)))) (\lambda (c3: C).(wf3 g c1 c3)) (\lambda (_: C).(\forall (w: T).((ty3 g
c1 v w) \to False))))) H4))))))))) y x H0))) H)))))).
+(* COMMENTS
+Initial nodes: 2507
+END *)
theorem wf3_gen_flat1:
\forall (g: G).(\forall (c1: C).(\forall (x: C).(\forall (v: T).(\forall (f:
(\lambda (c: C).((eq C c (CHead c1 (Flat f) v)) \to (wf3 g c1 c2))) H2 c1 H8)
in (let H10 \def (eq_ind C c0 (\lambda (c: C).(wf3 g c c2)) H1 c1 H8) in
H10))))) H5)) H4))))))))) y x H0))) H)))))).
+(* COMMENTS
+Initial nodes: 737
+END *)
theorem wf3_gen_head2:
\forall (g: G).(\forall (x: C).(\forall (c: C).(\forall (v: T).(\forall (k:
K k (Bind b)))))) H2 (CHead c k v) H4) in (let H6 \def (eq_ind C c2 (\lambda
(c0: C).(wf3 g c1 c0)) H1 (CHead c k v) H4) in (H5 (refl_equal C (CHead c k
v))))))))))))) x y H0))) H)))))).
+(* COMMENTS
+Initial nodes: 1225
+END *)