DEFINITION minus()
TYPE =
       nat→nat→nat
BODY =
FIXminus{
         minus:nat→nat→nat
         :=λn:nat
           .λm:nat
             .<λn1:nat.nat>
               CASE n OF
                 O⇒O
               | S k⇒<λn1:nat.nat> CASE m OF O⇒S k | S l⇒minus k l
         }