(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/wf3/fwd.ma".
+include "Basic-1/wf3/fwd.ma".
theorem wf3_clear_conf:
\forall (c1: C).(\forall (c: C).((clear c1 c) \to (\forall (g: G).(\forall
c0 c2)))))).(\lambda (f: F).(\lambda (u: T).(\lambda (g: G).(\lambda (c2:
C).(\lambda (H2: (wf3 g (CHead e (Flat f) u) c2)).(let H_y \def
(wf3_gen_flat1 g e c2 u f H2) in (H1 g c2 H_y))))))))))) c1 c H))).
+(* COMMENTS
+Initial nodes: 145
+END *)
theorem clear_wf3_trans:
\forall (c1: C).(\forall (d1: C).((clear c1 d1) \to (\forall (g: G).(\forall
(x: C).(\lambda (H4: (wf3 g e x)).(\lambda (H5: (clear x d2)).(ex_intro2 C
(\lambda (c2: C).(wf3 g (CHead e (Flat f) u) c2)) (\lambda (c2: C).(clear c2
d2)) x (wf3_flat g e x H4 u f) H5)))) H3)))))))))))) c1 d1 H))).
+(* COMMENTS
+Initial nodes: 1023
+END *)