fact: Definition var_decl_stmt typ name val := varDeclStmt (Statement := STATEMENT.t) (Block := BLOCK.t) (varDecl nil typ name) val.
imports: Coq(List) JML(ListHelpers) JML(JMLExpressionNotations) JML(JMLProgramPlusImpl)