Goal:
  
  A : Type
  B : Type
  l : list A
  f : ∀ x : A, In x l → B
  g : A → B
  hin : ∀ (x : A) (hin : In x l), f x hin = g x
  ============================
   (map_In l f = map_In l (λ (x : A) (_ : In x l), g x))


DEBUG:Going to execute:
apply map_In_ext
DEBUG LTAC Evaluated term: all_eq
DEBUG LTAC Evaluated term: map_In_spec
DEBUG LTAC Evaluated term: map_In_spec