proposition: Lemma iter_up_sound: forall S acc, ST.le (F (iter_up S acc)) (iter_up S acc).
proof: Proof. induction S using (well_founded_induction ST.widen_order_wf). intros acc. destruct acc. cbn. destruct (is_true (ST.ble (F S) S)). - apply ST.ble_1; auto. - apply H. exists (F S); auto. Qed.
imports: Coq(ZArith Psatz Bool String List FMaps) Coq(FunctionalExtensionality) CDF(Sequences IMP)