(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/sn3/defs.ma".
+include "Basic-1/sn3/defs.ma".
-include "LambdaDelta-1/pr3/props.ma".
+include "Basic-1/pr3/props.ma".
theorem sn3_gen_bind:
\forall (b: B).(\forall (c: C).(\forall (u: T).(\forall (t: T).((sn3 c
(CHead c (Bind b) x) t2) (sn3 (CHead c (Bind b) x) t2) (\lambda (_: (sn3 c
x)).(\lambda (H10: (sn3 (CHead c (Bind b) x) t2)).H10)) H8))))))))))))))) y
H0))))) H))))).
+(* COMMENTS
+Initial nodes: 1055
+END *)
theorem sn3_gen_flat:
\forall (f: F).(\forall (c: C).(\forall (u: T).(\forall (t: T).((sn3 c
T x0) P)))))) (pr3_thin_dx c x0 t2 H7 x f) x t2 (refl_equal T (THead (Flat f)
x t2))) in (land_ind (sn3 c x) (sn3 c t2) (sn3 c t2) (\lambda (_: (sn3 c
x)).(\lambda (H10: (sn3 c t2)).H10)) H8))))))))))))))) y H0))))) H))))).
+(* COMMENTS
+Initial nodes: 925
+END *)
theorem sn3_gen_head:
\forall (k: K).(\forall (c: C).(\forall (u: T).(\forall (t: T).((sn3 c
(Flat f) u t))).(let H_x \def (sn3_gen_flat f c u t H) in (let H0 \def H_x in
(land_ind (sn3 c u) (sn3 c t) (sn3 c u) (\lambda (H1: (sn3 c u)).(\lambda (_:
(sn3 c t)).H1)) H0)))))))) k).
+(* COMMENTS
+Initial nodes: 191
+END *)
theorem sn3_gen_cflat:
\forall (f: F).(\forall (c: C).(\forall (u: T).(\forall (t: T).((sn3 (CHead
(sn3 c t2)))))).(sn3_sing c t1 (\lambda (t2: T).(\lambda (H2: (((eq T t1 t2)
\to (\forall (P: Prop).P)))).(\lambda (H3: (pr3 c t1 t2)).(H1 t2 H2
(pr3_cflat c t1 t2 H3 f u))))))))) t H))))).
+(* COMMENTS
+Initial nodes: 175
+END *)
theorem sn3_gen_lift:
\forall (c1: C).(\forall (t: T).(\forall (h: nat).(\forall (d: nat).((sn3 c1
(\forall (P0: Prop).P0))) H7 x (lift_inj x t2 h d H9)) in (H11 (refl_equal T
x) P))))) (pr3_lift c1 c2 h d H4 x t2 H8) t2 (refl_equal T (lift h d t2)) c2
H4)))))))))))))) y H0)))) H))))).
+(* COMMENTS
+Initial nodes: 565
+END *)