proposition: Lemma In_fold_left_split' : forall bag l acc, List.In bag (acc ++ fold_left (fun (a0 : list BagType) (p : key * Trie) => Trie_enumerate (snd p) ++ a0) l [ ]) <-> List.In bag ((fold_left (fun (a0 : list BagType) (p : key * Trie) => Trie_enumerate (snd p) ++ a0) l acc)).
proof: Proof. induction l; simpl; intros. - rewrite app_nil_r in *; eauto. reflexivity. - rewrite <- IHl. split; intros. rewrite <- app_assoc; apply in_or_app. apply in_app_or in H; intuition eauto. right; apply in_or_app; eauto. rewrite <- IHl in H0. rewrite <- !app_assoc in H0. apply in_app_or in H0; intuition. apply in_app_or in H; intuition. apply in_app_or in H0; intuition. apply in_or_app; intuition. right; rewrite <- IHl; intuition. apply in_or_app; intuition. rewrite <- IHl in H0. apply in_app_or in H0; intuition. right. rewrite <- IHl. apply in_or_app; auto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsProperties Coq.FSets.FMapInterface Coq.FSets.FMapFacts Coq.FSets.FMapAVL Coq.ZArith.ZArith Fiat.Common Fiat.Common.List.ListFacts Fiat.Common.List.FlattenList Fiat.Common.SetEqProperties Fiat.Common.FMapExtensions Fiat.Common.List.PermutationFacts Fiat.QueryStructure.Specification.SearchTerms.ListPrefix