proposition: Lemma ToEnsemble_Size_refineEquiv fs (H : exists S0, forall S', S' ≅ S0 -> S' ≃ fs) : refineEquiv (ret (snd (CallMethod (projT1 FiniteSetImpl) sSize fs tt))) (cardinal (to_ensemble fs)).
proof: Proof. destruct H as [? H]. pose proof (H _ (reflexivity _)). apply ToEnsemble_Size_refineEquiv', 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