∀ (red green blue alpha red_1 green_1 blue_1 alpha_1 : Float),
  ({ red := red, green := green, blue := blue, alpha := alpha } =
      { red := red_1, green := green_1, blue := blue_1, alpha := alpha_1 }) =
    (red = red_1 ∧ green = green_1 ∧ blue = blue_1 ∧ alpha = alpha_1)