Definition componentValueWF (v : componentValueT) : Prop :=
  match v with
  | ValueIntegerS8 v      => integerS8TWF v
  | ValueIntegerS8Vec2 v  => integerS8Vec2TWF v
  | ValueIntegerS8Vec3 v  => integerS8Vec3TWF v
  | ValueIntegerS8Vec4 v  => integerS8Vec4TWF v
  | ValueIntegerU8 v      => integerU8TWF v
  | ValueIntegerU8Vec2 v  => integerU8Vec2TWF v
  | ValueIntegerU8Vec3 v  => integerU8Vec3TWF v
  | ValueIntegerU8Vec4 v  => integerU8Vec4TWF v
  | ValueIntegerS16 v     => integerS16TWF v
  | ValueIntegerS16Vec2 v => integerS16Vec2TWF v
  | ValueIntegerS16Vec3 v => integerS16Vec3TWF v
  | ValueIntegerS16Vec4 v => integerS16Vec4TWF v
  | ValueIntegerU16 v     => integerU16TWF v
  | ValueIntegerU16Vec2 v => integerU16Vec2TWF v
  | ValueIntegerU16Vec3 v => integerU16Vec3TWF v
  | ValueIntegerU16Vec4 v => integerU16Vec4TWF v
  | ValueIntegerS32 v     => integerS32TWF v
  | ValueIntegerS32Vec2 v => integerS32Vec2TWF v
  | ValueIntegerS32Vec3 v => integerS32Vec3TWF v
  | ValueIntegerS32Vec4 v => integerS32Vec4TWF v
  | ValueIntegerU32 v     => integerU32TWF v
  | ValueIntegerU32Vec2 v => integerU32Vec2TWF v
  | ValueIntegerU32Vec3 v => integerU32Vec3TWF v
  | ValueIntegerU32Vec4 v => integerU32Vec4TWF v
  | ValueIntegerS64 v     => integerS64TWF v
  | ValueIntegerS64Vec2 v => integerS64Vec2TWF v
  | ValueIntegerS64Vec3 v => integerS64Vec3TWF v
  | ValueIntegerS64Vec4 v => integerS64Vec4TWF v
  | ValueIntegerU64 v     => integerU64TWF v
  | ValueIntegerU64Vec2 v => integerU64Vec2TWF v
  | ValueIntegerU64Vec3 v => integerU64Vec3TWF v
  | ValueIntegerU64Vec4 v => integerU64Vec4TWF v
  | ValueFloat16 v        => float16TWF v
  | ValueFloat16Vec2 v    => float16Vec2TWF v
  | ValueFloat16Vec3 v    => float16Vec3TWF v
  | ValueFloat16Vec4 v    => float16Vec4TWF v
  | ValueFloat32 v        => float32TWF v
  | ValueFloat32Vec2 v    => float32Vec2TWF v
  | ValueFloat32Vec3 v    => float32Vec3TWF v
  | ValueFloat32Vec4 v    => float32Vec4TWF v
  | ValueFloat64 v        => float64TWF v
  | ValueFloat64Vec2 v    => float64Vec2TWF v
  | ValueFloat64Vec3 v    => float64Vec3TWF v
  | ValueFloat64Vec4 v    => float64Vec4TWF v
  end.
