proposition: Lemma finite_set_handle_EnsembleListEquivalence_iff' {A} (ls : list W) (f : _ -> Comp A) : refine (S <- { S : Ensemble W | forall x, Ensembles.In _ S x <-> List.In x ls }; Bind { ls' : _ | EnsembleListEquivalence S ls' } f) (f (snd (FiniteSetAndListOfList ls))).
proof: Proof. simpl. rewrite <- refineEquiv_bind_bind. rewrite finite_set_handle_EnsembleListEquivalence_iff; simpl. match goal with | [ |- context[ret ?x] ] => generalize x; intro end. autorewrite with refine_monad. reflexivity. 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