proposition: Lemma widen_1: forall N1 N2, le N1 (widen N1 N2).
proof: Proof. unfold widen; intros. destruct (ble N2 N1) eqn:LE. red; auto. red; unfold In; auto. Qed.
imports: Coq(ZArith Psatz Bool String List FMaps) Coq(FunctionalExtensionality) CDF(Sequences IMP)