fact: Definition rewriteVariant (lbl:Label) (e:Expression) : Expression := let lit0 := literal (IntLiteral 0%Z) in ( (lit0 <= e) &&' (e < \oldl e at lbl) )%jml.
imports: JML(Prelude) Coq(ZArith) Coq(Bool) Coq(List) JML(TaggedList) JML(ListHelpers) JML(ListFunctions) JML(OptionHelpers) JML(JMLProgramPlusImpl) JML(JMLFull2Basic) JML(JMLExpressionNotations)