proposition: Lemma finset_le_trans: forall x y z, finset_le x y -> finset_le y z -> finset_le x z.
proof: Proof. intros x y z; apply ISProp.subset_trans. Qed.
imports: Coq(ZArith Psatz Bool String Program.Equality FSets Wellfounded) CDF(Sequences IMP Simulation) CDF(Fixpoints)