no goals
U : Type ?u.1267
V : Type u_1
W : Type ?u.1273
inst✝² : Quiver U
inst✝¹ : Quiver V
inst✝ : Quiver W
h : HasInvolutiveReverse V
a b : V
f : a ⟶ b
g : b ⟶ a
⊢ f = reverse g ↔ reverse f = g
rw [←reverse_inj, reverse_reverse]