fact: Definition DecomposeRawQueryStructureSchema_AbsR' {m : nat} {qs_schema : QueryStructureSchema} ( schemaIdx' : BoundedIndex (QSschemaNames qs_schema)) (schemaIdx := ibound (indexb schemaIdx')) {attrIdx' : BoundedIndex (HeadingNames (QSGetNRelSchemaHeading (qs_schema) schemaIdx'))} (attrIdx := ibound (indexb attrIdx')) (attrIdx_inj : Fin.t _ -> Fin.t _) (EnumTypes : Vector.t Type m) (f' : Vector.nth (AttrList _) (attrIdx_inj attrIdx) -> SumType EnumTypes) (f'' : SumType EnumTypes -> Vector.nth (AttrList _) (attrIdx_inj attrIdx)) (a_proj_index : Vector.nth (AttrList _) (attrIdx_inj attrIdx) -> Fin.t m := fun attr => SumType_index EnumTypes (f' attr)) (a_proj : forall (attr : Vector.nth _ (attrIdx_inj attrIdx)), EnumTypes[@a_proj_index attr] := fun attr => SumType_proj EnumTypes (f' attr)) (a_inj : forall idx, Vector.nth EnumTypes idx -> Vector.nth (AttrList _) (attrIdx_inj attrIdx) := fun idx attr => f'' (inj_SumType EnumTypes idx attr)) (r_o : UnConstrQueryStructure qs_schema) (r_n : UnConstrQueryStructure qs_schema * UnConstrQueryStructure (DecomposeRawQueryStructureSchema qs_schema schemaIdx (attrIdx_inj attrIdx) EnumTypes)) : Prop := DecomposeRawQueryStructureSchema_AbsR (qs_schema := qs_schema) schemaIdx (attrIdx_inj attrIdx) EnumTypes a_proj_index a_proj a_inj r_o r_n.
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