proposition: Lemma Ensemble_fold_right_simpl' {A B} f b S : refineEquiv (@Ensemble_fold_right A B f b S) (ls <- to_list S; ret (List.fold_right f b ls)).
proof: Proof. exact (Ensemble_fold_right_simpl f b S). Qed.
imports: Coq.Classes.Morphisms Coq.Lists.List Fiat.ComputationalEnsembles.Core Fiat.Computation Fiat.Common.Ensembles.Tactics Fiat.Common.Ensembles