fact: Definition BuildHeading2 {n} (attrs : Vector.t Attribute2 n) : Heading2 := {| HeadingRaw2 := {| NumAttr2 := n; AttrList2 := Vector.map attrType2 attrs |}; HeadingNames2 := Vector.map attrName2 attrs |}.
imports: Coq.Lists.List Coq.Strings.String Coq.Logic.FunctionalExtensionality Coq.Sets.Ensembles Fiat.Common.ilist Fiat.Common.StringBound Coq.Program.Program Fiat.QueryStructure.Specification.Representation.Notations