proposition: Lemma InA_map_app {A B} (eqB : B -> B -> Prop) (f : A -> B) (e : B) : forall ls ls', InA eqB e (List.map f (ls ++ ls')) <-> InA eqB e (List.map f ls) \/ InA eqB e (List.map f ls').
proof: Proof. induction ls'; split; intros. - left. rewrite app_nil_r in H. auto. - destruct H. + rewrite app_nil_r. auto. + inversion H. - rewrite <- (InA_map_perm eqB f e (Permutation_middle ls ls' a)) in H. simpl in *. inversion H; subst. right. apply InA_cons_hd. assumption. rewrite IHls' in H1. inversion H1. left. assumption. right. apply InA_cons_tl. assumption. - rewrite <- (InA_map_perm eqB f e (Permutation_middle ls ls' a)). specialize (fun x => proj2 IHls' (or_introl x)). specialize (fun x => proj2 IHls' (or_intror x)). intros. simpl in *. inversion H. apply InA_cons_tl. eauto. inversion H2; subst. apply InA_cons_hd. eauto. apply InA_cons_tl. 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