DEFINITION ahead_inj_snd()
TYPE =
       ∀g:G.∀a1:A.∀a2:A.∀a3:A.∀a4:A.(leq g (AHead a1 a2) (AHead a3 a4))→(leq g a2 a4)
BODY =
Show proof