fact: Definition widen_aux (ov1 ov2: option V.t) : option V.t := match ov1, ov2 with | Some v1, Some v2 => Some (V.widen v1 v2) | None, _ => None | _, None => None end.
imports: Coq(ZArith Psatz Bool String List FMaps) Coq(FunctionalExtensionality) CDF(Sequences IMP)