proposition: Lemma Same_set_ToEnsemble_Remove fs x (H : exists S0, forall S', S' ≅ S0 -> S' ≃ fs) : to_ensemble (fst (CallMethod (projT1 FiniteSetImpl) sRemove fs x)) ≅ Ensembles.Subtract _ (to_ensemble fs) x.
proof: Proof. destruct H as [? H]. pose proof (H _ (reflexivity _)). apply Same_set_ToEnsemble_Remove', H; t. 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