proposition: Lemma refine_UnConstrQuery_In_DecomposeRawQueryStructureSchema_AbsR {m : nat} {qs_schema : RawQueryStructureSchema} {ResultT : Type} (schemaIdx : Fin.t _) (body : @RawTuple _ -> Comp (list ResultT)) (attrIdx : Fin.t _) a_proj el (r_o : UnConstrQueryStructure qs_schema) (r_n : UnConstrQueryStructure qs_schema * UnConstrQueryStructure (DecomposeRawQueryStructureSchema m qs_schema schemaIdx attrIdx)) : DecomposeRawQueryStructureSchema_AbsR schemaIdx attrIdx a_proj el r_o r_n -> refine (UnConstrQuery_In r_o schemaIdx body) (UnConstrQuery_In (fst r_n) schemaIdx body).
proof: Proof. intros. unfold UnConstrQuery_In, QueryResultComp; f_equiv. rewrite refine_UnIndexedEnsembleListEquivalence. reflexivity. intros. eapply UnIndexedEnsembleListEquivalence_Same_set; eauto. destruct H. unfold Same_set in *; intuition eauto. apply H. apply H. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Vectors.Vector Coq.Strings.Ascii Coq.Bool.Bool Coq.Lists.List Fiat.Common.SumType Fiat.Computation.ListComputations Fiat.QueryStructure.Automation.AutoDB Bedrock.Word Bedrock.Memory