proposition: Lemma ToEnsemble_In_refineEquiv fs x (H : exists S0, forall S', S' ≅ S0 -> S' ≃ fs) : refineEquiv (ret (snd (CallMethod (projT1 FiniteSetImpl) sIn fs x))) { b : bool | decides b (x ∈ to_ensemble fs) }.
proof: Proof. setoid_rewrite <- (@ToEnsemble_In_iff fs x H). setoid_rewrite refineEquiv_decides_eqb. rewrite refineEquiv_pick_eq; reflexivity. Qed.
imports: Coq.Strings.String Coq.Sets.Ensembles Coq.Sets.Finite_sets Coq.Lists.List Coq.Sorting.Permutation Fiat.ADT Fiat.ADT.ComputationalADT Fiat.ADTRefinement.Core Fiat.ADTNotation Fiat.ADTRefinement.GeneralRefinements Fiat.Common.Ensembles Fiat.FiniteSetADTs.FiniteSetADT Fiat.Common.Ensembles.Notations Fiat.Common.Ensembles.Equivalence