DEFINITION subst()
TYPE =
       nat→T→T→T
BODY =
Show proof