proposition: Lemma InA_map_forall {A B} : forall eqA eqB (f : A -> B) ls ls', Equivalence eqA -> Equivalence eqB -> Proper (eqA ==> eqB) f -> (forall a, InA eqA a ls -> InA eqA a ls') -> (forall b, InA eqB b (List.map f ls) -> InA eqB b (List.map f ls')).
proof: Proof. intros eqA eqB f ls ls' eqvA eqvB proper Hfa b H. unfold Proper, respectful in proper. generalize dependent ls'. generalize dependent ls. induction ls; intros. - inversion H. - inversion H; clear H; subst. + specialize (Hfa a (InA_cons_hd ls (reflexivity _))). induction Hfa. * simpl. constructor. rewrite H1. f_equiv. assumption. * simpl. constructor 2. assumption. + eauto. Qed.
imports: Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsProperties Coq.Arith.PeanoNat Coq.FSets.FMapInterface Coq.FSets.FMapFacts Coq.FSets.FMapAVL Fiat.Common Fiat.Common.List.ListFacts Fiat.Common.List.FlattenList Fiat.Common.SetEqProperties Fiat.Common.FMapExtensions Fiat.Common.List.PermutationFacts