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))
  ============================
   (map g (map_In (a :: xs) f) =
    map_In (a :: xs) (λ (x : X) (isin : In x (a :: xs)), g (f x isin)))


DEBUG:Going to execute:
idtac