proposition: Lemma refine_List_Query_In {ResultT} qsSchema qs R l resultComp : EnsembleIndexedListEquivalence (GetUnConstrRelation qs R) l -> refine (@UnConstrQuery_In ResultT qsSchema qs R resultComp) (List_Query_In l resultComp).
proof: Proof. intros; destruct H as [l' [eq_l_l' [eq_l_R equiv_l_R ] ] ]. intros; unfold UnConstrQuery_In, QueryResultComp, List_Query_In; rewrite refine_pick_val; unfold UnIndexedEnsembleListEquivalence; eauto. simplify with monad laws; subst; reflexivity. 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 Fiat.Common.List.ListFacts