fact: Definition mergeRequires (l0:list (optionalSame Expression)) : option (optionalSame Expression) := let liftOptionalSame2 (A:Type) (op:A->A->A) (oa ob:optionalSame A) : optionalSame A := match oa, ob with | SpecifiedOS a, SpecifiedOS b => SpecifiedOS (op a b) | NotSpecifiedOS, b => b | a, NotSpecifiedOS => a | same, _ => same | _, same => same end in match l0 with | nil => None | _ => Some (fold_left1 (liftOptionalSame2 Expression (BinaryCondBoolExpr ConditionalAnd)) l0 NotSpecifiedOS) end.
imports: JML(Prelude) Coq(ZArith) Coq(Bool) Coq(List) JML(TaggedList) JML(ListHelpers) JML(ListFunctions) JML(OptionHelpers) JML(JMLProgramPlusImpl) JML(JMLFull2Basic) JML(JMLExpressionNotations)