fact: Definition widen (N1 N2: t) : t := if isempty N1 then N2 else if isempty N2 then N1 else {| low := Zinf.widen (low N1) (low N2); high := Zinf.widen (high N1) (high N2) |}.
imports: Coq(ZArith Psatz Bool String List FMaps) Coq(FunctionalExtensionality) CDF(Sequences IMP)