DEFINITION nf2_gen_flat()
TYPE =
       ∀f:F.∀c:C.∀u:T.∀t:T.(nf2 c (THead (Flat f) u t))→(land (nf2 c u) (nf2 c t))
BODY =
        assume f: F
        assume c: C
        assume u: T
        assume t: T
          we must prove (nf2 c (THead (Flat f) u t))→(land (nf2 c u) (nf2 c t))
          or equivalently 
                ∀t2:T.(pr2 c (THead (Flat f) u t) t2)→(eq T (THead (Flat f) u t) t2)
                  →land (nf2 c u) (nf2 c t)
          suppose H: ∀t2:T.(pr2 c (THead (Flat f) u t) t2)→(eq T (THead (Flat f) u t) t2)
             (h1) 
                 assume t2: T
                 suppose H0: pr2 c u t2
                   (H1) 
                      by (pr2_head_1 . . . H0 . .)
                      we proved pr2 c (THead (Flat f) u t) (THead (Flat f) t2 t)
                      by (H . previous)
                      we proved eq T (THead (Flat f) u t) (THead (Flat f) t2 t)
                      by (f_equal . . . . . previous)
                      we proved 
                         eq
                           T
                           <λ:T.T> CASE THead (Flat f) u t OF TSort ⇒u | TLRef ⇒u | THead  t0 ⇒t0
                           <λ:T.T> CASE THead (Flat f) t2 t OF TSort ⇒u | TLRef ⇒u | THead  t0 ⇒t0

                         eq
                           T
                           λe:T.<λ:T.T> CASE e OF TSort ⇒u | TLRef ⇒u | THead  t0 ⇒t0
                             THead (Flat f) u t
                           λe:T.<λ:T.T> CASE e OF TSort ⇒u | TLRef ⇒u | THead  t0 ⇒t0
                             THead (Flat f) t2 t
                   end of H1
                   consider H1
                   we proved 
                      eq
                        T
                        <λ:T.T> CASE THead (Flat f) u t OF TSort ⇒u | TLRef ⇒u | THead  t0 ⇒t0
                        <λ:T.T> CASE THead (Flat f) t2 t OF TSort ⇒u | TLRef ⇒u | THead  t0 ⇒t0
                   that is equivalent to eq T u t2
∀t2:T.(pr2 c u t2)→(eq T u t2)
             end of h1
             (h2) 
                 assume t2: T
                 suppose H0: pr2 c t t2
                   (H1) 
                      by (pr2_cflat . . . H0 . .)
                      we proved pr2 (CHead c (Flat f) u) t t2
                      by (pr2_head_2 . . . . . previous)
                      we proved pr2 c (THead (Flat f) u t) (THead (Flat f) u t2)
                      by (H . previous)
                      we proved eq T (THead (Flat f) u t) (THead (Flat f) u t2)
                      by (f_equal . . . . . previous)
                      we proved 
                         eq
                           T
                           <λ:T.T> CASE THead (Flat f) u t OF TSort ⇒t | TLRef ⇒t | THead   t0⇒t0
                           <λ:T.T> CASE THead (Flat f) u t2 OF TSort ⇒t | TLRef ⇒t | THead   t0⇒t0

                         eq
                           T
                           λe:T.<λ:T.T> CASE e OF TSort ⇒t | TLRef ⇒t | THead   t0⇒t0
                             THead (Flat f) u t
                           λe:T.<λ:T.T> CASE e OF TSort ⇒t | TLRef ⇒t | THead   t0⇒t0
                             THead (Flat f) u t2
                   end of H1
                   consider H1
                   we proved 
                      eq
                        T
                        <λ:T.T> CASE THead (Flat f) u t OF TSort ⇒t | TLRef ⇒t | THead   t0⇒t0
                        <λ:T.T> CASE THead (Flat f) u t2 OF TSort ⇒t | TLRef ⇒t | THead   t0⇒t0
                   that is equivalent to eq T t t2
∀t2:T.(pr2 c t t2)→(eq T t t2)
             end of h2
             by (conj . . h1 h2)
             we proved land ∀t2:T.(pr2 c u t2)→(eq T u t2) ∀t2:T.(pr2 c t t2)→(eq T t t2)
             that is equivalent to land (nf2 c u) (nf2 c t)
          we proved 
             ∀t2:T.(pr2 c (THead (Flat f) u t) t2)→(eq T (THead (Flat f) u t) t2)
               →land (nf2 c u) (nf2 c t)
          that is equivalent to (nf2 c (THead (Flat f) u t))→(land (nf2 c u) (nf2 c t))
       we proved ∀f:F.∀c:C.∀u:T.∀t:T.(nf2 c (THead (Flat f) u t))→(land (nf2 c u) (nf2 c t))