DEFINITION dnf_dec()
TYPE =
       ∀w:T
         .∀t:T
           .∀d:nat
             .ex T λv:T.or (subst0 d w t (lift (S O) d v)) (eq T t (lift (S O) d v))
BODY =
        assume w: T
        assume t: T
        assume d: nat
          (H_x) 
             by (dnf_dec2 . .)

                or
                  ∀w:T.(ex T λv:T.subst0 d w t (lift (S O) d v))
                  ex T λv:T.eq T t (lift (S O) d v)
          end of H_x
          (H) consider H_x
          we proceed by induction on H to prove ex T λv:T.or (subst0 d w t (lift (S O) d v)) (eq T t (lift (S O) d v))
             case or_introl : H0:∀w0:T.(ex T λv:T.subst0 d w0 t (lift (S O) d v)) ⇒
                the thesis becomes ex T λv:T.or (subst0 d w t (lift (S O) d v)) (eq T t (lift (S O) d v))
                   (H_x0) 
                      by (H0 .)
ex T λv:T.subst0 d w t (lift (S O) d v)
                   end of H_x0
                   (H1) consider H_x0
                   we proceed by induction on H1 to prove ex T λv:T.or (subst0 d w t (lift (S O) d v)) (eq T t (lift (S O) d v))
                      case ex_intro : x:T H2:subst0 d w t (lift (S O) d x) ⇒
                         the thesis becomes ex T λv:T.or (subst0 d w t (lift (S O) d v)) (eq T t (lift (S O) d v))
                            by (or_introl . . H2)
                            we proved or (subst0 d w t (lift (S O) d x)) (eq T t (lift (S O) d x))
                            by (ex_intro . . . previous)
ex T λv:T.or (subst0 d w t (lift (S O) d v)) (eq T t (lift (S O) d v))
ex T λv:T.or (subst0 d w t (lift (S O) d v)) (eq T t (lift (S O) d v))
             case or_intror : H0:ex T λv:T.eq T t (lift (S O) d v) ⇒
                the thesis becomes ex T λv:T.or (subst0 d w t (lift (S O) d v)) (eq T t (lift (S O) d v))
                   we proceed by induction on H0 to prove ex T λv:T.or (subst0 d w t (lift (S O) d v)) (eq T t (lift (S O) d v))
                      case ex_intro : x:T H1:eq T t (lift (S O) d x) ⇒
                         the thesis becomes ex T λv:T.or (subst0 d w t (lift (S O) d v)) (eq T t (lift (S O) d v))
                            by (refl_equal . .)
                            we proved eq T (lift (S O) d x) (lift (S O) d x)
                            by (or_intror . . previous)
                            we proved 
                               or
                                 subst0 d w (lift (S O) d x) (lift (S O) d x)
                                 eq T (lift (S O) d x) (lift (S O) d x)
                            by (ex_intro . . . previous)
                            we proved 
                               ex
                                 T
                                 λv:T
                                   .or
                                     subst0 d w (lift (S O) d x) (lift (S O) d v)
                                     eq T (lift (S O) d x) (lift (S O) d v)
                            by (eq_ind_r . . . previous . H1)
ex T λv:T.or (subst0 d w t (lift (S O) d v)) (eq T t (lift (S O) d v))
ex T λv:T.or (subst0 d w t (lift (S O) d v)) (eq T t (lift (S O) d v))
          we proved ex T λv:T.or (subst0 d w t (lift (S O) d v)) (eq T t (lift (S O) d v))
       we proved 
          ∀w:T
            .∀t:T
              .∀d:nat
                .ex T λv:T.or (subst0 d w t (lift (S O) d v)) (eq T t (lift (S O) d v))