proposition: Lemma finset_eq_le: forall x y, finset_eq x y -> finset_le y x.
proof: Proof. intros. apply ISProp.subset_equal. apply ISProp.equal_sym. apply H. Qed.
imports: Coq(ZArith Psatz Bool String Program.Equality FSets Wellfounded) CDF(Sequences IMP Simulation) CDF(Fixpoints)