fact: Definition desugarNested (specs:list FULL_SPEC_CASE.t) : list FULL_SPEC_CASE.t := let desugar1 (spec:FULL_SPEC_CASE.t) : list FULL_SPEC_CASE.t := let (sct,v,r,cc,case) := spec in map (FULL_SPEC_CASE.Build_t sct v r cc) (flatten case) in flat_map desugar1 specs.
imports: JML(Prelude) Coq(ZArith) Coq(Bool) Coq(List) JML(TaggedList) JML(ListHelpers) JML(ListFunctions) JML(OptionHelpers) JML(JMLProgramPlusImpl) JML(JMLFull2Basic) JML(JMLExpressionNotations)