DEFINITION nf2_gen_abbr()
TYPE =
       ∀c:C.∀u:T.∀t:T.(nf2 c (THead (Bind Abbr) u t))→∀P:Prop.P
BODY =
        assume c: C
        assume u: T
        assume t: T
          we must prove (nf2 c (THead (Bind Abbr) u t))→∀P:Prop.P
          or equivalently 
                ∀t2:T
                    .pr2 c (THead (Bind Abbr) u t) t2
                      →eq T (THead (Bind Abbr) u t) t2
                  →∀P:Prop.P
           suppose H: 
              ∀t2:T
                .pr2 c (THead (Bind Abbr) u t) t2
                  →eq T (THead (Bind Abbr) u t) t2
           assume P: Prop
             (H_x) 
                by (dnf_dec . . .)
ex T λv:T.or (subst0 O u t (lift (S O) O v)) (eq T t (lift (S O) O v))
             end of H_x
             (H0) consider H_x
             we proceed by induction on H0 to prove P
                case ex_intro : x:T H1:or (subst0 O u t (lift (S O) O x)) (eq T t (lift (S O) O x)) ⇒
                   the thesis becomes P
                      we proceed by induction on H1 to prove P
                         case or_introl : H2:subst0 O u t (lift (S O) O x) ⇒
                            the thesis becomes P
                               (H3) 
                                  (h1) by (pr0_refl .) we proved pr0 u u
                                  (h2) by (pr0_refl .) we proved pr0 t t
                                  by (pr0_delta . . h1 . . h2 . H2)
                                  we proved 
                                     pr0
                                       THead (Bind Abbr) u t
                                       THead (Bind Abbr) u (lift (S O) O x)
                                  by (pr2_free . . . previous)
                                  we proved 
                                     pr2
                                       c
                                       THead (Bind Abbr) u t
                                       THead (Bind Abbr) u (lift (S O) O x)
                                  by (H . previous)
                                  we proved 
                                     eq
                                       T
                                       THead (Bind Abbr) u t
                                       THead (Bind Abbr) u (lift (S O) O x)
                                  by (f_equal . . . . . previous)
                                  we proved 
                                     eq
                                       T
                                       <λ:T.T>
                                         CASE THead (Bind Abbr) u t OF
                                           TSort ⇒t
                                         | TLRef ⇒t
                                         | THead   t0⇒t0
                                       <λ:T.T>
                                         CASE THead (Bind Abbr) u (lift (S O) O x) 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 Abbr) u t
                                       λe:T.<λ:T.T> CASE e OF TSort ⇒t | TLRef ⇒t | THead   t0⇒t0
                                         THead (Bind Abbr) u (lift (S O) O x)
                               end of H3
                               (H4) 
                                  consider H3
                                  we proved 
                                     eq
                                       T
                                       <λ:T.T>
                                         CASE THead (Bind Abbr) u t OF
                                           TSort ⇒t
                                         | TLRef ⇒t
                                         | THead   t0⇒t0
                                       <λ:T.T>
                                         CASE THead (Bind Abbr) u (lift (S O) O x) OF
                                           TSort ⇒t
                                         | TLRef ⇒t
                                         | THead   t0⇒t0
                                  that is equivalent to eq T t (lift (S O) O x)
                                  we proceed by induction on the previous result to prove subst0 O u (lift (S O) O x) (lift (S O) O x)
                                     case refl_equal : ⇒
                                        the thesis becomes the hypothesis H2
subst0 O u (lift (S O) O x) (lift (S O) O x)
                               end of H4
                               by (subst0_refl . . . H4 .)
P
                         case or_intror : H2:eq T t (lift (S O) O x) ⇒
                            the thesis becomes P
                               (H3) 
                                  we proceed by induction on H2 to prove 
                                     ∀t2:T
                                       .pr2 c (THead (Bind Abbr) u (lift (S O) O x)) t2
                                         →eq T (THead (Bind Abbr) u (lift (S O) O x)) t2
                                     case refl_equal : ⇒
                                        the thesis becomes the hypothesis H

                                     ∀t2:T
                                       .pr2 c (THead (Bind Abbr) u (lift (S O) O x)) t2
                                         →eq T (THead (Bind Abbr) u (lift (S O) O x)) t2
                               end of H3
                               by (pr0_refl .)
                               we proved pr0 x x
                               by (pr0_zeta . not_abbr_abst . . previous .)
                               we proved pr0 (THead (Bind Abbr) u (lift (S O) O x)) x
                               by (pr2_free . . . previous)
                               we proved pr2 c (THead (Bind Abbr) u (lift (S O) O x)) x
                               by (H3 . previous)
                               we proved eq T (THead (Bind Abbr) u (lift (S O) O x)) x
                               by (nf2_gen__nf2_gen_aux . . . . previous .)
P
P
             we proved P
          we proved 
             ∀t2:T
                 .pr2 c (THead (Bind Abbr) u t) t2
                   →eq T (THead (Bind Abbr) u t) t2
               →∀P:Prop.P
          that is equivalent to (nf2 c (THead (Bind Abbr) u t))→∀P:Prop.P
       we proved ∀c:C.∀u:T.∀t:T.(nf2 c (THead (Bind Abbr) u t))→∀P:Prop.P