DEFINITION nf2_abst()
TYPE =
       ∀c:C
         .∀u:T
           .nf2 c u
             →∀b:B
                  .∀v:T
                    .∀t:T.(nf2 (CHead c (Bind b) v) t)→(nf2 c (THead (Bind Abst) u t))
BODY =
        assume c: C
        assume u: T
          we must prove 
                nf2 c u
                  →∀b:B
                       .∀v:T
                         .∀t:T.(nf2 (CHead c (Bind b) v) t)→(nf2 c (THead (Bind Abst) u t))
          or equivalently 
                ∀t2:T.(pr2 c u t2)→(eq T u t2)
                  →∀b:B
                       .∀v:T
                         .∀t:T.(nf2 (CHead c (Bind b) v) t)→(nf2 c (THead (Bind Abst) u t))
           suppose H: ∀t2:T.(pr2 c u t2)→(eq T u t2)
           assume b: B
           assume v: T
           assume t: T
             we must prove (nf2 (CHead c (Bind b) v) t)→(nf2 c (THead (Bind Abst) u t))
             or equivalently 
                   ∀t2:T.(pr2 (CHead c (Bind b) v) t t2)→(eq T t t2)
                     →nf2 c (THead (Bind Abst) u t)
             suppose H0: ∀t2:T.(pr2 (CHead c (Bind b) v) t t2)→(eq T t t2)
                we must prove nf2 c (THead (Bind Abst) u t)
                or equivalently 
                      ∀t2:T
                        .pr2 c (THead (Bind Abst) u t) t2
                          →eq T (THead (Bind Abst) u t) t2
                 assume t2: T
                 suppose H1: pr2 c (THead (Bind Abst) u t) t2
                   (H2) 
                      by (pr2_gen_abst . . . . H1)

                         ex3_2
                           T
                           T
                           λu2:T.λt2:T.eq T t2 (THead (Bind Abst) u2 t2)
                           λu2:T.λ:T.pr2 c u u2
                           λ:T.λt2:T.∀b:B.∀u:T.(pr2 (CHead c (Bind b) u) t t2)
                   end of H2
                   we proceed by induction on H2 to prove eq T (THead (Bind Abst) u t) t2
                      case ex3_2_intro : x0:T x1:T H3:eq T t2 (THead (Bind Abst) x0 x1) H4:pr2 c u x0 H5:∀b0:B.∀u0:T.(pr2 (CHead c (Bind b0) u0) t x1) ⇒
                         the thesis becomes eq T (THead (Bind Abst) u t) t2
                            (h1) 
                               by (refl_equal . .)
eq K (Bind Abst) (Bind Abst)
                            end of h1
                            (h2) by (H . H4) we proved eq T u x0
                            (h3) 
                               by (H5 . .)
                               we proved pr2 (CHead c (Bind b) v) t x1
                               by (H0 . previous)
eq T t x1
                            end of h3
                            by (f_equal3 . . . . . . . . . . . h1 h2 h3)
                            we proved eq T (THead (Bind Abst) u t) (THead (Bind Abst) x0 x1)
                            by (eq_ind_r . . . previous . H3)
eq T (THead (Bind Abst) u t) t2
                   we proved eq T (THead (Bind Abst) u t) t2
                we proved 
                   ∀t2:T
                     .pr2 c (THead (Bind Abst) u t) t2
                       →eq T (THead (Bind Abst) u t) t2
                that is equivalent to nf2 c (THead (Bind Abst) u t)
             we proved 
                ∀t2:T.(pr2 (CHead c (Bind b) v) t t2)→(eq T t t2)
                  →nf2 c (THead (Bind Abst) u t)
             that is equivalent to (nf2 (CHead c (Bind b) v) t)→(nf2 c (THead (Bind Abst) u t))
          we proved 
             ∀t2:T.(pr2 c u t2)→(eq T u t2)
               →∀b:B
                    .∀v:T
                      .∀t:T.(nf2 (CHead c (Bind b) v) t)→(nf2 c (THead (Bind Abst) u t))
          that is equivalent to 
             nf2 c u
               →∀b:B
                    .∀v:T
                      .∀t:T.(nf2 (CHead c (Bind b) v) t)→(nf2 c (THead (Bind Abst) u t))
       we proved 
          ∀c:C
            .∀u:T
              .nf2 c u
                →∀b:B
                     .∀v:T
                       .∀t:T.(nf2 (CHead c (Bind b) v) t)→(nf2 c (THead (Bind Abst) u t))