DEFINITION dnf_dec2()
TYPE =
       ∀t:T
         .∀d:nat
           .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)
BODY =
Show proof