proposition: Lemma finset_bot_smallest: forall x, finset_le finset_bot x.
proof: Proof. intros; red; fsetdec. Qed.
imports: Coq(ZArith Psatz Bool String Program.Equality FSets Wellfounded) CDF(Sequences IMP Simulation) CDF(Fixpoints)