Inductive valueHasType : componentValueT -> componentTypeT -> Prop :=
  | VTS8 :
    forall (v  : integerS8T) 
           (wf : componentValueWF (ValueIntegerS8 v)), 
      valueHasType (ValueIntegerS8 v) INTEGER_SIGNED_8
  | VTS8_VEC2 :
    forall (v  : integerS8Vec2T) 
           (wf : componentValueWF (ValueIntegerS8Vec2 v)), 
      valueHasType (ValueIntegerS8Vec2 v) INTEGER_SIGNED_8_VEC2
  | VTS8_VEC3 :
    forall (v  : integerS8Vec3T) 
           (wf : componentValueWF (ValueIntegerS8Vec3 v)), 
      valueHasType (ValueIntegerS8Vec3 v) INTEGER_SIGNED_8_VEC3
  | VTS8_VEC4 :
    forall (v  : integerS8Vec4T) 
           (wf : componentValueWF (ValueIntegerS8Vec4 v)), 
      valueHasType (ValueIntegerS8Vec4 v) INTEGER_SIGNED_8_VEC4
  | VTU8 :
    forall (v  : integerU8T) 
           (wf : componentValueWF (ValueIntegerU8 v)), 
      valueHasType (ValueIntegerU8 v) INTEGER_UNSIGNED_8
  | VTU8_VEC2 :
    forall (v  : integerU8Vec2T) 
           (wf : componentValueWF (ValueIntegerU8Vec2 v)), 
      valueHasType (ValueIntegerU8Vec2 v) INTEGER_UNSIGNED_8_VEC2
  | VTU8_VEC3 :
    forall (v  : integerU8Vec3T) 
           (wf : componentValueWF (ValueIntegerU8Vec3 v)), 
      valueHasType (ValueIntegerU8Vec3 v) INTEGER_UNSIGNED_8_VEC3
  | VTU8_VEC4 :
    forall (v  : integerU8Vec4T) 
           (wf : componentValueWF (ValueIntegerU8Vec4 v)), 
      valueHasType (ValueIntegerU8Vec4 v) INTEGER_UNSIGNED_8_VEC4

  | VTS16 :
    forall (v  : integerS16T) 
           (wf : componentValueWF (ValueIntegerS16 v)), 
      valueHasType (ValueIntegerS16 v) INTEGER_SIGNED_16
  | VTS16_VEC2 :
    forall (v  : integerS16Vec2T) 
           (wf : componentValueWF (ValueIntegerS16Vec2 v)), 
      valueHasType (ValueIntegerS16Vec2 v) INTEGER_SIGNED_16_VEC2
  | VTS16_VEC3 :
    forall (v  : integerS16Vec3T) 
           (wf : componentValueWF (ValueIntegerS16Vec3 v)), 
      valueHasType (ValueIntegerS16Vec3 v) INTEGER_SIGNED_16_VEC3
  | VTS16_VEC4 :
    forall (v  : integerS16Vec4T) 
           (wf : componentValueWF (ValueIntegerS16Vec4 v)), 
      valueHasType (ValueIntegerS16Vec4 v) INTEGER_SIGNED_16_VEC4
  | VTU16 :
    forall (v  : integerU16T) 
           (wf : componentValueWF (ValueIntegerU16 v)), 
      valueHasType (ValueIntegerU16 v) INTEGER_UNSIGNED_16
  | VTU16_VEC2 :
    forall (v  : integerU16Vec2T) 
           (wf : componentValueWF (ValueIntegerU16Vec2 v)), 
      valueHasType (ValueIntegerU16Vec2 v) INTEGER_UNSIGNED_16_VEC2
  | VTU16_VEC3 :
    forall (v  : integerU16Vec3T) 
           (wf : componentValueWF (ValueIntegerU16Vec3 v)), 
      valueHasType (ValueIntegerU16Vec3 v) INTEGER_UNSIGNED_16_VEC3
  | VTU16_VEC4 :
    forall (v  : integerU16Vec4T) 
           (wf : componentValueWF (ValueIntegerU16Vec4 v)), 
      valueHasType (ValueIntegerU16Vec4 v) INTEGER_UNSIGNED_16_VEC4

  | VTS32 :
    forall (v  : integerS32T) 
           (wf : componentValueWF (ValueIntegerS32 v)), 
      valueHasType (ValueIntegerS32 v) INTEGER_SIGNED_32
  | VTS32_VEC2 :
    forall (v  : integerS32Vec2T) 
           (wf : componentValueWF (ValueIntegerS32Vec2 v)), 
      valueHasType (ValueIntegerS32Vec2 v) INTEGER_SIGNED_32_VEC2
  | VTS32_VEC3 :
    forall (v  : integerS32Vec3T) 
           (wf : componentValueWF (ValueIntegerS32Vec3 v)), 
      valueHasType (ValueIntegerS32Vec3 v) INTEGER_SIGNED_32_VEC3
  | VTS32_VEC4 :
    forall (v  : integerS32Vec4T) 
           (wf : componentValueWF (ValueIntegerS32Vec4 v)), 
      valueHasType (ValueIntegerS32Vec4 v) INTEGER_SIGNED_32_VEC4
  | VTU32 :
    forall (v  : integerU32T) 
           (wf : componentValueWF (ValueIntegerU32 v)), 
      valueHasType (ValueIntegerU32 v) INTEGER_UNSIGNED_32
  | VTU32_VEC2 :
    forall (v  : integerU32Vec2T) 
           (wf : componentValueWF (ValueIntegerU32Vec2 v)), 
      valueHasType (ValueIntegerU32Vec2 v) INTEGER_UNSIGNED_32_VEC2
  | VTU32_VEC3 :
    forall (v  : integerU32Vec3T) 
           (wf : componentValueWF (ValueIntegerU32Vec3 v)), 
      valueHasType (ValueIntegerU32Vec3 v) INTEGER_UNSIGNED_32_VEC3
  | VTU32_VEC4 :
    forall (v  : integerU32Vec4T) 
           (wf : componentValueWF (ValueIntegerU32Vec4 v)), 
      valueHasType (ValueIntegerU32Vec4 v) INTEGER_UNSIGNED_32_VEC4

  | VTS64 :
    forall (v  : integerS64T) 
           (wf : componentValueWF (ValueIntegerS64 v)), 
      valueHasType (ValueIntegerS64 v) INTEGER_SIGNED_64
  | VTS64_VEC2 :
    forall (v  : integerS64Vec2T) 
           (wf : componentValueWF (ValueIntegerS64Vec2 v)), 
      valueHasType (ValueIntegerS64Vec2 v) INTEGER_SIGNED_64_VEC2
  | VTS64_VEC3 :
    forall (v  : integerS64Vec3T) 
           (wf : componentValueWF (ValueIntegerS64Vec3 v)), 
      valueHasType (ValueIntegerS64Vec3 v) INTEGER_SIGNED_64_VEC3
  | VTS64_VEC4 :
    forall (v  : integerS64Vec4T) 
           (wf : componentValueWF (ValueIntegerS64Vec4 v)), 
      valueHasType (ValueIntegerS64Vec4 v) INTEGER_SIGNED_64_VEC4
  | VTU64 :
    forall (v  : integerU64T) 
           (wf : componentValueWF (ValueIntegerU64 v)), 
      valueHasType (ValueIntegerU64 v) INTEGER_UNSIGNED_64
  | VTU64_VEC2 :
    forall (v  : integerU64Vec2T) 
           (wf : componentValueWF (ValueIntegerU64Vec2 v)), 
      valueHasType (ValueIntegerU64Vec2 v) INTEGER_UNSIGNED_64_VEC2
  | VTU64_VEC3 :
    forall (v  : integerU64Vec3T) 
           (wf : componentValueWF (ValueIntegerU64Vec3 v)), 
      valueHasType (ValueIntegerU64Vec3 v) INTEGER_UNSIGNED_64_VEC3
  | VTU64_VEC4 :
    forall (v  : integerU64Vec4T) 
           (wf : componentValueWF (ValueIntegerU64Vec4 v)), 
      valueHasType (ValueIntegerU64Vec4 v) INTEGER_UNSIGNED_64_VEC4

  | VTF16 :
    forall (v  : float16T)
           (wf : componentValueWF (ValueFloat16 v)),
      valueHasType (ValueFloat16 v) FLOAT_16
  | VTF16_VEC2 :
    forall (v  : float16Vec2T)
           (wf : componentValueWF (ValueFloat16Vec2 v)),
      valueHasType (ValueFloat16Vec2 v) FLOAT_16_VEC2
  | VTF16_VEC3 :
    forall (v  : float16Vec3T)
           (wf : componentValueWF (ValueFloat16Vec3 v)),
      valueHasType (ValueFloat16Vec3 v) FLOAT_16_VEC3
  | VTF16_VEC4 :
    forall (v  : float16Vec4T)
           (wf : componentValueWF (ValueFloat16Vec4 v)),
      valueHasType (ValueFloat16Vec4 v) FLOAT_16_VEC4

  | VTF32 :
    forall (v  : float32T)
           (wf : componentValueWF (ValueFloat32 v)),
      valueHasType (ValueFloat32 v) FLOAT_32
  | VTF32_VEC2 :
    forall (v  : float32Vec2T)
           (wf : componentValueWF (ValueFloat32Vec2 v)),
      valueHasType (ValueFloat32Vec2 v) FLOAT_32_VEC2
  | VTF32_VEC3 :
    forall (v  : float32Vec3T)
           (wf : componentValueWF (ValueFloat32Vec3 v)),
      valueHasType (ValueFloat32Vec3 v) FLOAT_32_VEC3
  | VTF32_VEC4 :
    forall (v  : float32Vec4T)
           (wf : componentValueWF (ValueFloat32Vec4 v)),
      valueHasType (ValueFloat32Vec4 v) FLOAT_32_VEC4

  | VTF64 :
    forall (v  : float64T)
           (wf : componentValueWF (ValueFloat64 v)),
      valueHasType (ValueFloat64 v) FLOAT_64
  | VTF64_VEC2 :
    forall (v  : float64Vec2T)
           (wf : componentValueWF (ValueFloat64Vec2 v)),
      valueHasType (ValueFloat64Vec2 v) FLOAT_64_VEC2
  | VTF64_VEC3 :
    forall (v  : float64Vec3T)
           (wf : componentValueWF (ValueFloat64Vec3 v)),
      valueHasType (ValueFloat64Vec3 v) FLOAT_64_VEC3
  | VTF64_VEC4 :
    forall (v  : float64Vec4T)
           (wf : componentValueWF (ValueFloat64Vec4 v)),
      valueHasType (ValueFloat64Vec4 v) FLOAT_64_VEC4
.
