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


DEBUG:Going to execute:
f_equal