DEFINITION asucc_gen_head()
TYPE =
       ∀g:G
         .∀a1:A
           .∀a2:A
             .∀a:A
               .eq A (AHead a1 a2) (asucc g a)
                 →ex2 A λa0:A.eq A a (AHead a1 a0) λa0:A.eq A a2 (asucc g a0)
BODY =
Show proof