fact: Definition filterTag (t:tag) (l:list data) : list Expression := let f := fun x => match x with exist _ (_,d) _ => d end in map f (filterTag tag tag_eq_dec data tagOf t l).
imports: JML(Prelude) Coq(ZArith) Coq(Bool) Coq(List) JML(TaggedList) JML(ListHelpers) JML(ListFunctions) JML(OptionHelpers) JML(JMLProgramPlusImpl) JML(JMLFull2Basic) JML(JMLExpressionNotations)