proposition: Lemma finite_set_handle_cardinal_helper (ls : list W) : refine (S <- { S : Ensemble W | forall x, Ensembles.In _ S x <-> List.In x ls }; FiniteSetADT.cardinal S) (ret (snd (CallMethod (projT1 FiniteSetImpl) sSize (FiniteSetOfList ls) tt))).
proof: Proof. etransitivity; [ | apply comp_split_snd ]. handle_calls; [ | apply AbsR_EnsembleOfList_FiniteSetOfList ]. repeat first [ progress simpl | rewrite <- refine_skip | autosetoid_rewrite with refine_monad ]. repeat intro; eauto. Qed.
imports: Coq.Strings.String Coq.Sets.Ensembles Coq.Sets.Finite_sets Coq.Lists.List Coq.Sorting.Permutation Coq.Classes.RelationPairs Fiat.ADT Fiat.ADT.ComputationalADT Fiat.ADTRefinement.Core Fiat.ADTNotation Fiat.ADTRefinement.GeneralRefinements Fiat.Computation Fiat.Common Fiat.Common.Ensembles Fiat.Common.Ensembles.Tactics Fiat.ComputationalEnsembles Fiat.FiniteSetADTs.FiniteSetADTMethodLaws Fiat.FiniteSetADTs.FiniteSetADT