cases g₂
case r120
g₂ : Rotation
p : State
⊢ r120 + g₂ +ᵥ p = r120 +ᵥ (g₂ +ᵥ p)
case r120.r0
p : State
⊢ r120 + r0 +ᵥ p = r120 +ᵥ (r0 +ᵥ p)

case r120.r120
p : State
⊢ r120 + r120 +ᵥ p = r120 +ᵥ (r120 +ᵥ p)

case r120.r240
p : State
⊢ r120 + r240 +ᵥ p = r120 +ᵥ (r240 +ᵥ p)