fact: Definition liftOptional1 (A B:Type) (op:A->B) (oa:optional A) : optional B := match oa with | Specified a => Specified (op a) | NotSpecified => NotSpecified end.
imports: JML(Prelude) Coq(ZArith) Coq(Bool) Coq(List) JML(TaggedList) JML(ListHelpers) JML(ListFunctions) JML(OptionHelpers) JML(JMLProgramPlusImpl) JML(JMLFull2Basic) JML(JMLExpressionNotations)