proposition: Lemma Join_Filtered_Comp_Lists_ExtensionalEq_filters {n} {A : Type} {f : A -> Type} {As : Vector.t A n} {a : A} : forall (l' : list (ilist2 (B := f) As)) (c : ilist2 (B := f) As -> Comp (list (f a))) (g g' : ilist2 (B := f) (a :: As) -> bool), ExtensionalEq g g' -> refine (Join_Filtered_Comp_Lists l' c g) (Join_Filtered_Comp_Lists l' c g').
proof: Proof. unfold Join_Filtered_Comp_Lists; intros. f_equiv; intro. f_equiv; apply filter_by_equiv; eauto. Qed.
imports: Coq.Arith.Arith Coq.ZArith.ZArith Coq.NArith.NArith Coq.ZArith.ZArith Coq.Strings.String Coq.Lists.List Coq.Sorting.Permutation Coq.Bool.Bool Coq.Sets.Ensembles Coq.Logic.FunctionalExtensionality Fiat.ADTNotation Fiat.Common Fiat.Common.ilist2 Fiat.Common.List.ListFacts Fiat.Common.Ensembles.IndexedEnsembles Fiat.Common.DecideableEnsembles Fiat.Computation Fiat.ADTRefinement.BuildADTRefinements Fiat.QueryStructure.Specification.Representation.QueryStructureSchema Fiat.QueryStructure.Specification.Operations.FlattenCompList Fiat.QueryStructure.Specification.Operations.Query Fiat.QueryStructure.Specification.Representation.QueryStructure