Definition structureValueHasStructureType
  (structVal  : structureValueT)
  (structType : structureT)
: Prop :=
  let fValues := structureComponentValues structVal in
  let fTypes  := structureComponents structType in
    length fValues = length fTypes /\ componentValuesHaveTypes (combine fValues fTypes).
