DEFINITION aplus()
TYPE =
       G→A→nat→A
BODY =
FIXaplus{
         aplus:G→A→nat→A
         :=λg:G.λa:A.λn:nat.<λn1:nat.A> CASE n OF O⇒a | S n0⇒asucc g (aplus g a n0)
         }