Goal:
    A : Type  y : A  l' : list A  h : All2 eq l' l'
  ============================
   (y :: l' = y :: l')


DEBUG:Going to execute:
reflexivity