DEFINITION blt()
TYPE =
       nat→nat→bool
BODY =
Show proof