proposition: Lemma refine_Iterate_Equiv_QueryResultComp {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) (Iterate_Equiv_QueryResultComp_body _ _ (GetUnConstrRelation (snd r_n)) (fun idx => Tuple_DecomposeRawQueryStructure_inj _ _ (el idx) idx) body).
proof: Proof. intros. erewrite refine_UnConstrQuery_In_DecomposeRawQueryStructureSchema_AbsR by eassumption. rewrite <- refine_Iterate_Equiv_QueryResultComp_body. unfold UnConstrQuery_In, QueryResultComp; f_equiv. rewrite refine_UnIndexedEnsembleListEquivalence. - unfold DecomposeRawQueryStructureSchema; simpl. intros; rewrite <- refine_UnIndexedEnsembleListEquivalence_Iterate_Equiv_QueryResultComp. + reflexivity. + intros; destruct H as [? [? [? [? ?] ] ] ]. intro; pose proof (H5 _ _ _ _ H1 H2 H0); simpl in *; eauto. - unfold UnIndexedEnsembleListEquivalence; simpl; intros. destruct_ex; intuition; subst. eexists x; intuition eauto. apply H in H1. apply H0. eexists _, _; split; eauto. simpl; destruct x0; simpl; f_equal. symmetry; apply Tuple_DecomposeRawQueryStructure_inj_inverse. unfold In in *; apply H0 in H1; destruct_ex; intuition; subst. apply (proj1 (proj2 H)) in H4; eassumption. 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