fact: Definition assume (e:Expression) (l:option Expression):= LocalAssumption (Statement := STATEMENT.t) (Block := BLOCK.t) e l false.
imports: Coq(List) JML(ListHelpers) JML(JMLExpressionNotations) JML(JMLProgramPlusImpl)