DEFINITION nf2_gen_beta()
TYPE =
       ∀c:C
         .∀u:T
           .∀v:T
             .∀t:T
               .nf2 c (THead (Flat Appl) u (THead (Bind Abst) v t))
                 →∀P:Prop.P
BODY =
        assume c: C
        assume u: T
        assume v: T
        assume t: T
          we must prove 
                nf2 c (THead (Flat Appl) u (THead (Bind Abst) v t))
                  →∀P:Prop.P
          or equivalently 
                ∀t2:T
                    .pr2 c (THead (Flat Appl) u (THead (Bind Abst) v t)) t2
                      →eq T (THead (Flat Appl) u (THead (Bind Abst) v t)) t2
                  →∀P:Prop.P
           suppose H: 
              ∀t2:T
                .pr2 c (THead (Flat Appl) u (THead (Bind Abst) v t)) t2
                  →eq T (THead (Flat Appl) u (THead (Bind Abst) v t)) t2
           assume P: Prop
             (H0) 
                (h1) by (pr0_refl .) we proved pr0 u u
                (h2) by (pr0_refl .) we proved pr0 t t
                by (pr0_beta . . . h1 . . h2)
                we proved 
                   pr0
                     THead (Flat Appl) u (THead (Bind Abst) v t)
                     THead (Bind Abbr) u t
                by (pr2_free . . . previous)
                we proved 
                   pr2
                     c
                     THead (Flat Appl) u (THead (Bind Abst) v t)
                     THead (Bind Abbr) u t
                by (H . previous)
                we proved 
                   eq
                     T
                     THead (Flat Appl) u (THead (Bind Abst) v t)
                     THead (Bind Abbr) u t
                we proceed by induction on the previous result to prove 
                   <λ:T.Prop>
                     CASE THead (Bind Abbr) u t OF
                       TSort ⇒False
                     | TLRef ⇒False
                     | THead k  ⇒<λ:K.Prop> CASE k OF Bind ⇒False | Flat ⇒True
                   case refl_equal : ⇒
                      the thesis becomes 
                      <λ:T.Prop>
                        CASE THead (Flat Appl) u (THead (Bind Abst) v t) OF
                          TSort ⇒False
                        | TLRef ⇒False
                        | THead k  ⇒<λ:K.Prop> CASE k OF Bind ⇒False | Flat ⇒True
                         consider I
                         we proved True

                            <λ:T.Prop>
                              CASE THead (Flat Appl) u (THead (Bind Abst) v t) OF
                                TSort ⇒False
                              | TLRef ⇒False
                              | THead k  ⇒<λ:K.Prop> CASE k OF Bind ⇒False | Flat ⇒True

                   <λ:T.Prop>
                     CASE THead (Bind Abbr) u t OF
                       TSort ⇒False
                     | TLRef ⇒False
                     | THead k  ⇒<λ:K.Prop> CASE k OF Bind ⇒False | Flat ⇒True
             end of H0
             consider H0
             we proved 
                <λ:T.Prop>
                  CASE THead (Bind Abbr) u t OF
                    TSort ⇒False
                  | TLRef ⇒False
                  | THead k  ⇒<λ:K.Prop> CASE k OF Bind ⇒False | Flat ⇒True
             that is equivalent to False
             we proceed by induction on the previous result to prove P
             we proved P
          we proved 
             ∀t2:T
                 .pr2 c (THead (Flat Appl) u (THead (Bind Abst) v t)) t2
                   →eq T (THead (Flat Appl) u (THead (Bind Abst) v t)) t2
               →∀P:Prop.P
          that is equivalent to 
             nf2 c (THead (Flat Appl) u (THead (Bind Abst) v t))
               →∀P:Prop.P
       we proved 
          ∀c:C
            .∀u:T
              .∀v:T
                .∀t:T
                  .nf2 c (THead (Flat Appl) u (THead (Bind Abst) v t))
                    →∀P:Prop.P