proposition: Lemma FiniteSet_AbsR_Same_set fs (S0 S1 : Ensemble W) (H0 : S0 ≃ fs) (H1 : S1 ≃ fs) : S0 ≅ S1.
proof: Proof. lazy; split; intros; match goal with | [ H : ?S' ≃ ?fs, H' : ?S'' ≃ ?fs |- ?S' ?x ] => pose proof (let f := ADTRefinementPreservesMethods (projT2 FiniteSetImpl) {| bindex := "In"%string |} S' _ x H in f _ (ReturnComputes _)); pose proof (let f := ADTRefinementPreservesMethods (projT2 FiniteSetImpl) {| bindex := "In"%string |} S'' _ x H' in f _ (ReturnComputes _)); simpl in * end; repeat t_pre_step. 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