proposition: Lemma FiniteSetAndFunctionOfList_proper {A} (R : relation A) (f f' : W -> A -> A) (a a' : A) (ls : list W) (Rf : pointwise_relation _ (respectful R R) f f') (RA : R a a') : R (snd (FiniteSetAndFunctionOfList f a ls)) (snd (FiniteSetAndFunctionOfList f' a' ls)).
proof: Proof. unfold pointwise_relation, respectful in *. revert a a' RA. induction ls; simpl; trivial. intros. rewrite !NoFunctionJustFiniteSetOfFunction. match goal with | [ |- context[if ?E then _ else _] ] => destruct E; auto end. 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