DEFINITION plus()
TYPE =
       nat→nat→nat
BODY =
FIXplus{
         plus:nat→nat→nat
         :=λn:nat.λm:nat.<λn1:nat.nat> CASE n OF O⇒m | S p⇒S (plus p m)
         }