fact: Fixpoint iter (n: nat) (x: IdentSet.t) : IdentSet.t := match n with | O => default | S n' => let x' := F x in if IdentSet.subset x' x then x else iter n' x' end.
imports: Coq(ZArith Psatz Bool String Program.Equality FSets Wellfounded) CDF(Sequences IMP Simulation)