proposition: Lemma InA_map_perm {A B} (eqB : B -> B -> Prop) (f : A -> B) (e : B) : forall ls ls', Permutation ls ls' -> (InA eqB e (List.map f ls) <-> InA eqB e (List.map f ls')).
proof: Proof. induction 1; intuition. - inversion H2; subst. apply InA_cons_hd. auto. simpl. apply InA_cons_tl. apply H0. auto. - inversion H2; subst. apply InA_cons_hd. auto. simpl. apply InA_cons_tl. apply H1. auto. - inversion H; subst; simpl. apply InA_cons_tl. apply InA_cons_hd. auto. inversion H1; subst; simpl. apply InA_cons_hd. auto. apply InA_cons_tl. apply InA_cons_tl. auto. - inversion H; subst; simpl. apply InA_cons_tl. apply InA_cons_hd. auto. inversion H1; subst; simpl. apply InA_cons_hd. auto. apply InA_cons_tl. apply InA_cons_tl. auto. 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