Goal:
  
  X : Type
  Y : Type
  xs : list X
  f : ∀ x : X, In x xs → Y
  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)


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

Goals:
    X : Type  Y : Type  f : ∀ x : X, In x [] → Y  g : ∀ x : X, In x [] → Y
  ============================
   ((∀ (x : X) (isin : In x []), f x isin = g x isin)
    → map_In [] f = map_In [] g)

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


DEBUG:Going to execute:
intros all_eq
DEBUG LTAC Evaluated term: xs