proposition: Lemma postfixpoint_sound: ST.le (F postfixpoint) postfixpoint.
proof: Proof. apply iter_down_sound. apply iter_up_sound. Qed.
imports: Coq(ZArith Psatz Bool String List FMaps) Coq(FunctionalExtensionality) CDF(Sequences IMP)