case mp
U : Type ?u.753
V : Type u_1
W : Type ?u.759
inst✝² : Quiver U
inst✝¹ : Quiver V
inst✝ : Quiver W
h : HasInvolutiveReverse V
a b : V
f g : a ⟶ b
⊢ reverse f = reverse g → f = g

case mpr
U : Type ?u.753
V : Type u_1
W : Type ?u.759
inst✝² : Quiver U
inst✝¹ : Quiver V
inst✝ : Quiver W
h : HasInvolutiveReverse V
a b : V
f g : a ⟶ b
⊢ f = g → reverse f = reverse g
U : Type ?u.753
V : Type u_1
W : Type ?u.759
inst✝² : Quiver U
inst✝¹ : Quiver V
inst✝ : Quiver W
h : HasInvolutiveReverse V
a b : V
f g : a ⟶ b
⊢ reverse f = reverse g ↔ f = g
constructor
case mp
U : Type ?u.753
V : Type u_1
W : Type ?u.759
inst✝² : Quiver U
inst✝¹ : Quiver V
inst✝ : Quiver W
h✝ : HasInvolutiveReverse V
a b : V
f g : a ⟶ b
h : reverse f = reverse g
⊢ f = g
case mp
U : Type ?u.753
V : Type u_1
W : Type ?u.759
inst✝² : Quiver U
inst✝¹ : Quiver V
inst✝ : Quiver W
h : HasInvolutiveReverse V
a b : V
f g : a ⟶ b
⊢ reverse f = reverse g → f = g
rintro h
no goals
case mp
U : Type ?u.753
V : Type u_1
W : Type ?u.759
inst✝² : Quiver U
inst✝¹ : Quiver V
inst✝ : Quiver W
h✝ : HasInvolutiveReverse V
a b : V
f g : a ⟶ b
h : reverse f = reverse g
⊢ f = g
simpa using congr_arg Quiver.reverse h
case mpr
U : Type ?u.753
V : Type u_1
W : Type ?u.759
inst✝² : Quiver U
inst✝¹ : Quiver V
inst✝ : Quiver W
h✝ : HasInvolutiveReverse V
a b : V
f g : a ⟶ b
h : f = g
⊢ reverse f = reverse g
case mpr
U : Type ?u.753
V : Type u_1
W : Type ?u.759
inst✝² : Quiver U
inst✝¹ : Quiver V
inst✝ : Quiver W
h : HasInvolutiveReverse V
a b : V
f g : a ⟶ b
⊢ f = g → reverse f = reverse g
rintro h
no goals
case mpr
U : Type ?u.753
V : Type u_1
W : Type ?u.759
inst✝² : Quiver U
inst✝¹ : Quiver V
inst✝ : Quiver W
h✝ : HasInvolutiveReverse V
a b : V
f g : a ⟶ b
h : f = g
⊢ reverse f = reverse g
congr