proposition: Lemma EnsembleListEquivalence_Intersection_Singleton' (x : W) (S0 : Ensemble W) : refine { ls' : _ | EnsembleListEquivalence (Intersection W S0 (Singleton _ x)) ls' } (ls_S0 <- to_list S0; let fs_S0 := FiniteSetOfList ls_S0 in ret (if (snd (CallMethod (projT1 FiniteSetImpl) sIn fs_S0 x) : bool) then x::nil else nil)).
proof: Proof. setoid_rewrite Intersection_sym. apply EnsembleListEquivalence_Intersection_Singleton. 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