fact: Definition assert_redundantly (e:Expression) (l:option Expression) := LocalAssertion (Statement := STATEMENT.t) (Block := BLOCK.t) e l true.
imports: Coq(List) JML(ListHelpers) JML(JMLExpressionNotations) JML(JMLProgramPlusImpl)