FancyMap.v

From Coq Require Import List.

Fixpoint map_In {A B : Type} (xs : list A) : (forall x, In x xs -> B) -> list B :=
  match xs return (forall x, In x xs -> B) -> list B with
  | nil => fun _ => nil
  | cons x xs' => fun f => cons (f x (or_introl eq_refl)) (map_In xs' (fun x' In_x'_xs' => f x' (or_intror In_x'_xs')))
  end.