proposition: Lemma fold_right_snd_FiniteSetAndListOfList {A} (f : W -> A -> A) (a : A) ls : List.fold_right f a (snd (FiniteSetAndListOfList ls)) = snd (FiniteSetAndFunctionOfList f a ls).
proof: Proof. simpl. induction ls; simpl; trivial. unfold FiniteSetAndListOfList in *. rewrite <- IHls. rewrite !NoFunctionJustFiniteSetOfFunction. match goal with | [ |- context[if ?x then _ else _] ] => case_eq x; intro 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