DEFINITION aprem_gen_head_S()
TYPE =
       ∀a1:A.∀a2:A.∀x:A.∀i:nat.(aprem (S i) (AHead a1 a2) x)→(aprem i a2 x)
BODY =
Show proof