fact: Definition monotone (F: finset -> finset) : Prop := forall x y, finset_le x y -> finset_le (F x) (F y).
imports: Coq(ZArith Psatz Bool String Program.Equality FSets Wellfounded) CDF(Sequences IMP Simulation) CDF(Fixpoints)