fact: Definition simple_case forallVarDecl oldVarDecl specHeader (simple:list MethodSpecClause) := GENERIC_SPEC_CASE.Build_t forallVarDecl oldVarDecl specHeader (inl _ simple).
imports: Coq(List) JML(ListHelpers) JML(JMLExpressionNotations) JML(JMLProgramPlusImpl)