a1 a3) (AHead a1 a4))) (\lambda (a4: A).(eq A (asucc g a3) (asucc g a4))) a3
(refl_equal A (AHead a1 a3)) (refl_equal A (asucc g a3))) a2 H3))) a0 H4))))
H2))))))) a)))).
a1 a3) (AHead a1 a4))) (\lambda (a4: A).(eq A (asucc g a3) (asucc g a4))) a3
(refl_equal A (AHead a1 a3)) (refl_equal A (asucc g a3))) a2 H3))) a0 H4))))
H2))))))) a)))).