proposition: Lemma Ensemble_fold_right_simpl {A B} (f : A -> B -> B) b S : refineEquiv (@fold_right A B (fun a b' => ret (f a b')) (ret b) S) (ls <- to_list S; ret (List.fold_right f b ls)).
proof: Proof. unfold fold_right. f_equiv; intro ls; simpl. induction ls; simpl; try reflexivity. rewrite IHls. autorewrite with refine_monad. reflexivity. Qed.
imports: Coq.Classes.Morphisms Coq.Lists.List Fiat.ComputationalEnsembles.Core Fiat.Computation Fiat.Common.Ensembles.Tactics Fiat.Common.Ensembles