proposition: Lemma FunctionOfList_pick_in b0 ls S0 : refine (FunctionOfList (fun (a : W) (b' : Comp (list W)) => xs <- b'; b <- {b : bool | b = true <-> Ensembles.In W S0 a}; ret (if b then a :: xs else xs)) b0 ls) (ls' <- to_list S0; let fs_S0 := FiniteSetOfList ls' in FunctionOfList (fun (a : W) (b' : Comp (list W)) => (xs <- b'; ret (if (snd (CallMethod (projT1 FiniteSetImpl) sIn fs_S0 a) : bool) then a :: xs else xs))) b0 ls).
proof: Proof. FunctionOfList_pick_t S0. 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