proposition: Lemma Tuple_DecomposeRawQueryStructure_inj_inverse {m : nat} {qs_schema : RawQueryStructureSchema} : forall (schemaIdx : Fin.t _) (attrIdx : Fin.t _) (a : Vector.t Type m) (a_proj_index : Vector.nth (AttrList (GetNRelSchemaHeading (qschemaSchemas qs_schema) schemaIdx)) attrIdx -> Fin.t m) (a_proj : forall (attr : Vector.nth _ attrIdx), a[@a_proj_index attr]) (a_inj : forall idx, Vector.nth a idx -> Vector.nth (AttrList (GetNRelSchemaHeading (qschemaSchemas qs_schema) schemaIdx)) attrIdx) tup, Tuple_DecomposeRawQueryStructure_inj' schemaIdx attrIdx a a_inj (a_proj_index (GetAttributeRaw tup attrIdx)) (Tuple_DecomposeRawQueryStructure_proj' schemaIdx attrIdx a a_proj_index a_proj tup) = tup.
proof: Proof. Admitted. Lemma ith_replace2_Index_eq': forall (A : Type) (B : A -> Type) (m : nat) (n n' : Fin.t m) (As : t A m) (il : ilist2 As) (new_b : B As[@n']) (H : n' = n), ith2 (replace_Index2 As il n' new_b) n = @eq_rect _ _ (fun n => B As[@n]) new_b _ H. Proof. intros. subst; unfold eq_rect; apply ith_replace2_Index_eq. 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