Goal:
  
  X : Type
  Y : Type
  a : X
  xs : list X
  f : ∀ x : X, In x (a :: xs) → Y
  g : ∀ x : X, In x (a :: xs) → Y
  IHxs : ∀ f g : ∀ x : X, In x xs → Y,
           (∀ (x : X) (isin : In x xs), f x isin = g x isin)
           → map_In xs f = map_In xs g
  all_eq : ∀ (x : X) (isin : In x (a :: xs)), f x isin = g x isin
  ============================
   (f a (map_In_obligations_obligation_1 X a xs)
    :: map_In xs
         (λ (x : X) (H : In x xs),
            f x (map_In_obligations_obligation_2 X a xs x H)) =
    g a (map_In_obligations_obligation_1 X a xs)
    :: map_In xs
         (λ (x : X) (H : In x xs),
            g x (map_In_obligations_obligation_2 X a xs x H)))


DEBUG:Going to execute:
f_equal