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


DEBUG:Going to execute:
trivial with eq_true