proposition: Lemma finset_fixpoint_smallest: forall F M z, finset_le (F z) z -> finset_le (finset_fixpoint F M) z.
proof: Proof. intros. unfold finset_fixpoint. apply fixpoint_smallest; eauto using finset_le_trans. Qed.
imports: Coq(ZArith Psatz Bool String Program.Equality FSets Wellfounded) CDF(Sequences IMP Simulation) CDF(Fixpoints)