fact: Fixpoint filterTag (t:tag) (l:list data) : list {d:data | t=tagOf d} := match l with | nil => nil | d1::ll => let t1 := tagOf d1 in match tag_eq_dec t t1 return list {d:data | t=tagOf d} with | left Heq => (exist (fun d : data => t = tagOf d) d1 Heq) :: (filterTag t ll) | right _ => filterTag t ll end end.
imports: Coq(List) Coq(Decidable)