rw [← inv_rotate_inv A l.inv]
V : Sort u_1
inst✝ : SerreGraph V
A : V
l : Loop A
⊢ HEq (rotate' A (inv l)) (inv (rotate A l))
V : Sort u_1
inst✝ : SerreGraph V
A : V
l : Loop A
⊢ HEq (inv (rotate A (inv (inv l)))) (inv (rotate A l))