DEFINITION aplus()
TYPE =
       G→A→nat→A
BODY =
Show proof