proposition: Remark isempty_widen: forall N1 N2, isempty N1 = false -> isempty N2 = false -> isempty (widen N1 N2) = false.
proof: Proof. intros. destruct (isempty (widen N1 N2)) eqn:E; auto. destruct (isempty_2 _ H) as (n1 & IN1). elim (isempty_1 n1 _ E). apply widen_1; auto. Qed.
imports: Coq(ZArith Psatz Bool String List FMaps) Coq(FunctionalExtensionality) CDF(Sequences IMP)