repeat {
  cases g₂
  repeat {
    cases p
    repeat rfl
  }
}
case r0
g₂ : Rotation
p : State
⊢ r0 + g₂ +ᵥ p = r0 +ᵥ (g₂ +ᵥ p)

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

case r240
g₂ : Rotation
p : State
⊢ r240 + g₂ +ᵥ p = r240 +ᵥ (g₂ +ᵥ p)
no goals