DEFINITION aprem_gen_head_O()
TYPE =
       ∀a1:A.∀a2:A.∀x:A.(aprem O (AHead a1 a2) x)→(eq A x a1)
BODY =
Show proof