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


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