proposition: Lemma finset_fixpoint_mon: forall F1 M1 F2 M2, (forall x, finset_le (F1 x) (F2 x)) -> finset_le (finset_fixpoint F1 M1) (finset_fixpoint F2 M2).
proof: Proof. intros. unfold finset_fixpoint. apply fixpoint_mon; eauto using finset_le_trans, finset_eq_le. Qed.
imports: Coq(ZArith Psatz Bool String Program.Equality FSets Wellfounded) CDF(Sequences IMP Simulation) CDF(Fixpoints)