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