Goal:
  
  A : Type
  B : Type
  f : A → B
  a : A
  l : list A
  l' : list A
  l'' : list A
  ============================
   (chop 0 (a :: l) = (l', l'')
    → chop 0 (map f (a :: l)) = (map f l', map f l''))


DEBUG:Going to execute:
intros [=<- <-]