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


DEBUG:Going to execute:
induction xs in xs, f |- *