fact: Definition DecomposeSchema' (heading : RawSchema) (attr : Fin.t (NumAttr (rawSchemaHeading heading))) : RawSchema := match attr in Fin.t n' return Vector.t _ n' -> RawSchema with | Fin.F1 _ => fun v => {| rawSchemaHeading := {| AttrList := BreakdownHeading Fin.F1 v |}; attrConstraints := None; tupleConstraints := None |} | Fin.FS _ attr' => fun v => {| rawSchemaHeading := {| AttrList := BreakdownHeading (Fin.FS attr') v |}; attrConstraints := None; tupleConstraints := None |} end (AttrList (rawSchemaHeading heading)).
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