fact: Definition mergeForallVarDecl (l:list FORALL_VAR_DECL.t) : option FORALL_VAR_DECL.t := match l with | nil => None | _ => Some (FORALL_VAR_DECL.Build_t (flat_map FORALL_VAR_DECL.vars l)) end.
imports: JML(Prelude) Coq(ZArith) Coq(Bool) Coq(List) JML(TaggedList) JML(ListHelpers) JML(ListFunctions) JML(OptionHelpers) JML(JMLProgramPlusImpl) JML(JMLFull2Basic) JML(JMLExpressionNotations)