DEFINITION aprem_asucc()
TYPE =
       ∀g:G.∀a1:A.∀a2:A.∀i:nat.(aprem i a1 a2)→(aprem i (asucc g a1) a2)
BODY =
Show proof