proposition: Lemma In_fold_right_app {A} : forall (l : list (list A)) (l'' : list A) (a : A), List.In a (fold_right (@app _) l'' l) <-> (List.In a l'' \/ (exists l', List.In l' l /\ List.In a l')).
proof: Proof. induction l; simpl; intuition. destruct_ex; intuition. apply in_app_or in H; intuition; eauto. destruct (proj1 (IHl _ _) H0); intuition. destruct_ex; intuition; eauto. eapply in_or_app; right; eapply IHl; intuition. destruct_ex; intuition; subst; eauto. eapply in_or_app; left; eauto. eapply in_or_app; right; eapply IHl; eauto. Qed.
imports: Coq.Strings.String Coq.ZArith.ZArith Coq.Lists.List Coq.Logic.FunctionalExtensionality Coq.Sets.Ensembles Coq.Sorting.Permutation Fiat.Computation Fiat.ADT Fiat.ADTRefinement Fiat.ADTNotation Fiat.ADTRefinement.GeneralBuildADTRefinements Fiat.QueryStructure.Specification.Representation.QueryStructureSchema Fiat.QueryStructure.Specification.Operations.Query Fiat.QueryStructure.Specification.Representation.QueryStructure Fiat.QueryStructure.Implementation.Operations.General.QueryRefinements Fiat.Common.SetEq Fiat.Common.Ensembles.IndexedEnsembles Fiat.Common.DecideableEnsembles Fiat.Common.List.ListMorphisms Fiat.Common.List.FlattenList Fiat.QueryStructure.Specification.Operations.FlattenCompList