proposition: Lemma postfixpoint_sound: ST.le (F postfixpoint) postfixpoint.
proof: Proof. unfold postfixpoint. generalize niter ST.bot. induction n; intros S; cbn. - red; intros; apply ST.top_1. - destruct (ST.ble (F S) S) eqn:B. + apply ST.ble_1; auto. + apply IHn. Qed.
imports: Coq(ZArith Psatz Bool String List FMaps) CDF(Sequences IMP)