proposition: Lemma finite_set_handle_cardinal (S : Ensemble W) : refine (FiniteSetADT.cardinal S) (ls <- { ls : _ | EnsembleListEquivalence S ls }; ret (snd (CallMethod (projT1 FiniteSetImpl) sSize (FiniteSetOfList ls) tt))).
proof: Proof. simpl. setoid_rewrite <- finite_set_handle_cardinal_helper. rewrite reverse_ensemble_list_equivalence_iff'. rewrite <- refine_skip2. repeat intro; inversion_by computes_to_inv. match goal with | [ H : _ ≅ _, H' : computes_to ?a ?v |- computes_to ?b ?v ] => revert v H'; change (refine b a); rewrite H end. reflexivity. 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