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 =
Show proof