repeat {
  cases p
  repeat rfl
}
case r240.r0
p : State
⊢ r240 + r0 +ᵥ p = r240 +ᵥ (r0 +ᵥ p)

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

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