DEFINITION subst()
TYPE =
       nat→T→T→T
BODY =
FIXsubst{
         subst:nat→T→T→T
         :=λd:nat
           .λv:T
             .λt:T
               .<λt1:T.T>
                 CASE t OF
                   TSort n⇒TSort n
                 | TLRef i⇒
                       <λb:bool.T>
                         CASE blt i d OF
                           true⇒TLRef i
                         | false⇒
                               <λb:bool.T>
                                 CASE blt d i OF
                                   true⇒TLRef (pred i)
                                 | false⇒lift d O v
                 | THead k u t0⇒THead k (subst d v u) (subst (s k d) v t0)
         }