proposition: Lemma Same_set_ToEnsemble_Remove' fs S0 x (H : S0 ≃ fs) : to_ensemble (fst (CallMethod (projT1 FiniteSetImpl) sRemove fs x)) ≅ Ensembles.Subtract _ S0 x.
proof: Proof. apply Same_set_ToEnsemble_AbsR, AbsR_ToEnsemble_Remove; assumption. 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