proposition: Lemma Join_Comp_Lists_apply_f {n} {A B C : Type} {f : A -> Type} : forall (As : Vector.t A n) (a : A) (l : list (ilist2 (B := f) As)) (c : ilist2 (B := f) As -> Comp (list (f a))) (c' : B -> Comp C) (f' : list (ilist2 (B := f) (a :: As)) -> B), refineEquiv (l' <- Join_Comp_Lists l c; c' (f' l')) (l' <- (l' <- Join_Comp_Lists l c; ret (f' l')); c' l').
proof: Proof. split; rewrite refineEquiv_bind_bind; setoid_rewrite refineEquiv_bind_unit; intros v Comp_v; computes_to_inv; try econstructor; eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Lists.List Coq.Program.Program Fiat.QueryStructure.Specification.Representation.Tuple Fiat.QueryStructure.Specification.Representation.Heading Fiat.Common.ilist2 Fiat.Common.i2list Fiat.Common.ilist3 Fiat.Common.i3list Coq.Bool.Bool Coq.Strings.String Coq.Structures.OrderedTypeEx Coq.Arith.Arith Fiat.Common.String_as_OT Fiat.Common.Ensembles.IndexedEnsembles Fiat.Common.DecideableEnsembles Fiat.Common.List.ListFacts Fiat.QueryStructure.Specification.Operations.FlattenCompList Fiat.QueryStructure.Implementation.Operations.General.QueryRefinements Fiat.QueryStructure.Implementation.Operations.General.InsertRefinements Fiat.QueryStructure.Implementation.Operations.General.EmptyRefinements Fiat.QueryStructure.Specification.Representation.QueryStructureNotations Fiat.QueryStructure.Implementation.ListImplementation Fiat.Common.List.PermutationFacts Fiat.QueryStructure.Implementation.DataStructures.BagADT.BagADT Fiat.QueryStructure.Implementation.DataStructures.BagADT.QueryStructureImplementation Fiat.QueryStructure.Implementation.DataStructures.BagADT.IndexSearchTerms Fiat.QueryStructure.Implementation.Operations.General.DeleteRefinements