fact: Definition mapTag (f : forall t:tag, {d:data | t=tagOf d} -> data) (l:list data) : list data := let f' (d:data) : data := f (tagOf d) (exist _ d (refl_equal (tagOf d))) in List.map f' l.
imports: Coq(List) Coq(Decidable)