DEFINITION nf2_gen_abst()
TYPE =
       ∀c:C
         .∀u:T
           .∀t:T
             .nf2 c (THead (Bind Abst) u t)
               →land (nf2 c u) (nf2 (CHead c (Bind Abst) u) t)
BODY =
        assume c: C
        assume u: T
        assume t: T
          we must prove 
                nf2 c (THead (Bind Abst) u t)
                  →land (nf2 c u) (nf2 (CHead c (Bind Abst) u) t)
          or equivalently 
                ∀t2:T
                    .pr2 c (THead (Bind Abst) u t) t2
                      →eq T (THead (Bind Abst) u t) t2
                  →land (nf2 c u) (nf2 (CHead c (Bind Abst) u) t)
          suppose H: 
             ∀t2:T
               .pr2 c (THead (Bind Abst) u t) t2
                 →eq T (THead (Bind Abst) u t) t2
             (h1) 
                 assume t2: T
                 suppose H0: pr2 c u t2
                   (H1) 
                      by (pr2_head_1 . . . H0 . .)
                      we proved pr2 c (THead (Bind Abst) u t) (THead (Bind Abst) t2 t)
                      by (H . previous)
                      we proved eq T (THead (Bind Abst) u t) (THead (Bind Abst) t2 t)
                      by (f_equal . . . . . previous)
                      we proved 
                         eq
                           T
                           <λ:T.T>
                             CASE THead (Bind Abst) u t OF
                               TSort ⇒u
                             | TLRef ⇒u
                             | THead  t0 ⇒t0
                           <λ:T.T> CASE THead (Bind Abst) 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 (Bind Abst) u t
                           λe:T.<λ:T.T> CASE e OF TSort ⇒u | TLRef ⇒u | THead  t0 ⇒t0
                             THead (Bind Abst) t2 t
                   end of H1
                   consider H1
                   we proved 
                      eq
                        T
                        <λ:T.T>
                          CASE THead (Bind Abst) u t OF
                            TSort ⇒u
                          | TLRef ⇒u
                          | THead  t0 ⇒t0
                        <λ:T.T> CASE THead (Bind Abst) t2 t OF TSort ⇒u | TLRef ⇒u | THead  t0 ⇒t0
                   that is equivalent to eq T u t2
                   we proceed by induction on the previous result to prove eq T u t2
                      case refl_equal : ⇒
                         the thesis becomes eq T u u
                            by (refl_equal . .)
eq T u u
                   we proved eq T u t2
∀t2:T.(pr2 c u t2)→(eq T u t2)
             end of h1
             (h2) 
                 assume t2: T
                 suppose H0: pr2 (CHead c (Bind Abst) u) t t2
                   (H1) 
                      (H_y) 
                         by (pr2_gen_cbind . . . . . H0)
pr2 c (THead (Bind Abst) u t) (THead (Bind Abst) u t2)
                      end of H_y
                      consider H_y
                      we proved pr2 c (THead (Bind Abst) u t) (THead (Bind Abst) u t2)
                      by (H . previous)
                      we proved eq T (THead (Bind Abst) u t) (THead (Bind Abst) u t2)
                      by (f_equal . . . . . previous)
                      we proved 
                         eq
                           T
                           <λ:T.T>
                             CASE THead (Bind Abst) u t OF
                               TSort ⇒t
                             | TLRef ⇒t
                             | THead   t0⇒t0
                           <λ:T.T> CASE THead (Bind Abst) 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 (Bind Abst) u t
                           λe:T.<λ:T.T> CASE e OF TSort ⇒t | TLRef ⇒t | THead   t0⇒t0
                             THead (Bind Abst) u t2
                   end of H1
                   consider H1
                   we proved 
                      eq
                        T
                        <λ:T.T>
                          CASE THead (Bind Abst) u t OF
                            TSort ⇒t
                          | TLRef ⇒t
                          | THead   t0⇒t0
                        <λ:T.T> CASE THead (Bind Abst) u t2 OF TSort ⇒t | TLRef ⇒t | THead   t0⇒t0
                   that is equivalent to eq T t t2
                   we proceed by induction on the previous result to prove eq T t t2
                      case refl_equal : ⇒
                         the thesis becomes eq T t t
                            by (refl_equal . .)
eq T t t
                   we proved eq T t t2
∀t2:T.(pr2 (CHead c (Bind Abst) u) 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 (CHead c (Bind Abst) u) t t2)→(eq T t t2)
             that is equivalent to land (nf2 c u) (nf2 (CHead c (Bind Abst) u) t)
          we proved 
             ∀t2:T
                 .pr2 c (THead (Bind Abst) u t) t2
                   →eq T (THead (Bind Abst) u t) t2
               →land (nf2 c u) (nf2 (CHead c (Bind Abst) u) t)
          that is equivalent to 
             nf2 c (THead (Bind Abst) u t)
               →land (nf2 c u) (nf2 (CHead c (Bind Abst) u) t)
       we proved 
          ∀c:C
            .∀u:T
              .∀t:T
                .nf2 c (THead (Bind Abst) u t)
                  →land (nf2 c u) (nf2 (CHead c (Bind Abst) u) t)