proposition: Lemma reverse_ensemble_list_equivalence_iff' {B} (S : Ensemble W) (f : _ -> Comp B) : refineEquiv (ls <- {ls : list W | EnsembleListEquivalence S ls}; Bind {S0 : Ensemble W | forall x : W, Ensembles.In W S0 x <-> List.In x ls} f) (ls <- {ls : list W | EnsembleListEquivalence S ls}; Bind { S' : _ | Same_set _ S' S } f).
proof: Proof. etransitivity; [ symmetry; apply refineEquiv_bind_bind | ]. rewrite reverse_ensemble_list_equivalence_iff. apply refineEquiv_bind_bind. Qed.
imports: Coq.Strings.String Coq.Sets.Ensembles Coq.Sets.Finite_sets Coq.Lists.List Coq.Sorting.Permutation Coq.Classes.RelationPairs Fiat.ADT Fiat.ADT.ComputationalADT Fiat.ADTRefinement.Core Fiat.ADTNotation Fiat.ADTRefinement.GeneralRefinements Fiat.Computation Fiat.Common Fiat.Common.Ensembles Fiat.Common.Ensembles.Tactics Fiat.ComputationalEnsembles Fiat.FiniteSetADTs.FiniteSetADTMethodLaws Fiat.FiniteSetADTs.FiniteSetADT