(* This file was automatically generated: do not edit *********************)
+include "LambdaDelta-1/nf2/defs.ma".
+include "LambdaDelta-1/pr2/clen.ma".
-include "nf2/defs.ma".
+include "LambdaDelta-1/subst0/dec.ma".
-include "pr2/clen.ma".
-
-include "subst0/dec.ma".
-
-include "T/props.ma".
+include "LambdaDelta-1/T/props.ma".
theorem nf2_gen_lref:
\forall (c: C).(\forall (d: C).(\forall (u: T).(\forall (i: nat).((getl i c
\def
\lambda (c: C).(\lambda (u: T).(\lambda (t: T).(\lambda (H: (nf2 c (THead
(Flat Cast) u t))).(\lambda (P: Prop).(thead_x_y_y (Flat Cast) u t (H t
-(pr2_free c (THead (Flat Cast) u t) t (pr0_epsilon t t (pr0_refl t) u)))
-P))))).
+(pr2_free c (THead (Flat Cast) u t) t (pr0_tau t t (pr0_refl t) u))) P))))).
theorem nf2_gen_beta:
\forall (c: C).(\forall (u: T).(\forall (v: T).(\forall (t: T).((nf2 c
(THead (Flat f) u t) (THead (Flat f) u t2) (H (THead (Flat f) u t2)
(pr2_head_2 c u t t2 (Flat f) (pr2_cflat c t t2 H0 f u)))) in H1)))))))).
-theorem nf2_gen__aux:
+theorem nf2_gen__nf2_gen_aux:
\forall (b: B).(\forall (x: T).(\forall (u: T).(\forall (d: nat).((eq T
(THead (Bind b) u (lift (S O) d x)) x) \to (\forall (P: Prop).P)))))
\def
(subst0_refl u (lift (S O) O x) O H4 P)))) (\lambda (H2: (eq T t (lift (S O)
O x))).(let H3 \def (eq_ind T t (\lambda (t0: T).(\forall (t2: T).((pr2 c
(THead (Bind Abbr) u t0) t2) \to (eq T (THead (Bind Abbr) u t0) t2)))) H
-(lift (S O) O x) H2) in (nf2_gen__aux Abbr x u O (H3 x (pr2_free c (THead
-(Bind Abbr) u (lift (S O) O x)) x (pr0_zeta Abbr not_abbr_abst x x (pr0_refl
-x) u))) P))) H1))) H0))))))).
+(lift (S O) O x) H2) in (nf2_gen__nf2_gen_aux Abbr x u O (H3 x (pr2_free c
+(THead (Bind Abbr) u (lift (S O) O x)) x (pr0_zeta Abbr not_abbr_abst x x
+(pr0_refl x) u))) P))) H1))) H0))))))).
theorem nf2_gen_void:
\forall (c: C).(\forall (u: T).(\forall (t: T).((nf2 c (THead (Bind Void) u
\def
\lambda (c: C).(\lambda (u: T).(\lambda (t: T).(\lambda (H: ((\forall (t2:
T).((pr2 c (THead (Bind Void) u (lift (S O) O t)) t2) \to (eq T (THead (Bind
-Void) u (lift (S O) O t)) t2))))).(\lambda (P: Prop).(nf2_gen__aux Void t u O
-(H t (pr2_free c (THead (Bind Void) u (lift (S O) O t)) t (pr0_zeta Void
-not_void_abst t t (pr0_refl t) u))) P))))).
+Void) u (lift (S O) O t)) t2))))).(\lambda (P: Prop).(nf2_gen__nf2_gen_aux
+Void t u O (H t (pr2_free c (THead (Bind Void) u (lift (S O) O t)) t
+(pr0_zeta Void not_void_abst t t (pr0_refl t) u))) P))))).