\forall (t: T).(\forall (d: nat).(or (\forall (w: T).(ex T (\lambda (v:
T).(subst0 d w t (lift (S O) d v))))) (ex T (\lambda (v: T).(eq T t (lift (S
O) d v))))))
\forall (t: T).(\forall (d: nat).(or (\forall (w: T).(ex T (\lambda (v:
T).(subst0 d w t (lift (S O) d v))))) (ex T (\lambda (v: T).(eq T t (lift (S
O) d v))))))