wi))).(\lambda (vs: TList).(\lambda (_: (pc3 (CSort m) (THeads (Flat Appl) vs
(lift (S i) O wi)) (THead (Bind Abst) w u))).(getl_gen_sort m i (CHead d
(Bind Abst) wi) H False))))))))).
wi))).(\lambda (vs: TList).(\lambda (_: (pc3 (CSort m) (THeads (Flat Appl) vs
(lift (S i) O wi)) (THead (Bind Abst) w u))).(getl_gen_sort m i (CHead d
(Bind Abst) wi) H False))))))))).
TList).(\lambda (i: nat).(nf2 c (TLRef i)))))) (\lambda (x: A).(\lambda (H2:
(arity g c t x)).(\lambda (_: (arity g c u (asucc g x))).(arity_nf2_inv_all g
c t x H2 H0)))) H1)))))))).
TList).(\lambda (i: nat).(nf2 c (TLRef i)))))) (\lambda (x: A).(\lambda (H2:
(arity g c t x)).(\lambda (_: (arity g c u (asucc g x))).(arity_nf2_inv_all g
c t x H2 H0)))) H1)))))))).
theorem ty3_nf2_inv_sort:
\forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (m: nat).((ty3 g c t
theorem ty3_nf2_inv_sort:
\forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (m: nat).((ty3 g c t
nat).(nfs2 c ws))) (\lambda (_: TList).(\lambda (i: nat).(nf2 c (TLRef i))))
x0 x1 (refl_equal T (THeads (Flat Appl) x0 (TLRef x1))) H4 H5)) t H3)))))))
H2)) H1)))))))).
nat).(nfs2 c ws))) (\lambda (_: TList).(\lambda (i: nat).(nf2 c (TLRef i))))
x0 x1 (refl_equal T (THeads (Flat Appl) x0 (TLRef x1))) H4 H5)) t H3)))))))
H2)) H1)))))))).
theorem ty3_nf2_gen__ty3_nf2_inv_abst_aux:
\forall (c: C).(\forall (w1: T).(\forall (u1: T).((ty3_nf2_inv_abst_premise
theorem ty3_nf2_gen__ty3_nf2_inv_abst_aux:
\forall (c: C).(\forall (w1: T).(\forall (u1: T).((ty3_nf2_inv_abst_premise
(THeads (Flat Appl) vs (lift (S i) O wi))) (pc3_thin_dx c (THeads (Flat Appl)
vs (lift (S i) O wi)) (THead (Bind Abst) w2 u2) H2 t Appl) (THead (Bind Abst)
w1 u1) H0))))))))))))))).
(THeads (Flat Appl) vs (lift (S i) O wi))) (pc3_thin_dx c (THeads (Flat Appl)
vs (lift (S i) O wi)) (THead (Bind Abst) w2 u2) H2 t Appl) (THead (Bind Abst)
w1 u1) H0))))))))))))))).
theorem ty3_nf2_inv_abst:
\forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (w: T).(\forall (u:
theorem ty3_nf2_inv_abst:
\forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (w: T).(\forall (u:
v)))) H23)))))) t1 H18))))))) H17))))))))) (ty3_gen_appl g c t0 (THeads (Flat
Appl) t1 (TLRef x1)) (THead (Bind Abst) x x2) H12))))))))) x0)) H10)) H9)) t
H5))))))) H4)) H3))))))))))).
v)))) H23)))))) t1 H18))))))) H17))))))))) (ty3_gen_appl g c t0 (THeads (Flat
Appl) t1 (TLRef x1)) (THead (Bind Abst) x x2) H12))))))))) x0)) H10)) H9)) t
H5))))))) H4)) H3))))))))))).