fact: Fixpoint iter_up (S: ST.t) (acc: Acc ST.widen_order S) : ST.t := let S' := F S in match is_true (ST.ble S' S) with | left LE => S | right NOTLE => iter_up (ST.widen S S') (iter_up_acc S acc S' NOTLE) end.
imports: Coq(ZArith Psatz Bool String List FMaps) Coq(FunctionalExtensionality) CDF(Sequences IMP)