proposition: Lemma postfixpoint_upper_bound: IdentSet.Subset postfixpoint default.
proof: Proof. assert (REC: forall n x, IdentSet.Subset x default -> IdentSet.Subset (iter n x) default). { induction n; intros; cbn. - fsetdec. - destruct (IdentSet.subset (F x) x); auto. } apply REC. fsetdec. Qed.
imports: Coq(ZArith Psatz Bool String Program.Equality FSets Wellfounded) CDF(Sequences IMP Simulation)