fact: Definition rewriteProgram (p:Program) : Program := let (classes,interfaces) := p in let classes' := map rewriteTYPEDEF classes in let interfaces' := map rewriteTYPEDEF interfaces in PROG.Build_t classes' interfaces'.
imports: JML(JMLBasic2Minimal) JML(JMLSyntax) Coq(List)