DEFINITION asucc()
TYPE =
       G→A→A
BODY =
Show proof