proposition: Lemma AbsR_ToEnsemble_Remove S0 fs x (H : S0 ≃ fs) : Ensembles.Subtract _ S0 x ≃ fst (CallMethod (projT1 FiniteSetImpl) sRemove fs x).
proof: Proof. handle_methods; 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