V : Type u
inst✝ : Quiver V
X Y : Paths (Quiver.Symmetrify V)
p : X ⟶ Y
⊢ Quot.mk (Quotient.CompClosure redStep) (Quiver.Path.reverse p ≫ Quiver.Path.reverse (Quiver.Path.reverse p)) =
    Quot.mk (Quotient.CompClosure redStep) (𝟙 Y)
V : Type u
inst✝ : Quiver V
X Y : Paths (Quiver.Symmetrify V)
p : X ⟶ Y
⊢ Quot.mk (Quotient.CompClosure redStep) (Quiver.Path.reverse p ≫ p) = Quot.mk (Quotient.CompClosure redStep) (𝟙 Y)
nth_rw 2 [← Quiver.Path.reverse_reverse p]
no goals
V : Type u
inst✝ : Quiver V
X Y : Paths (Quiver.Symmetrify V)
p : X ⟶ Y
⊢ Quot.mk (Quotient.CompClosure redStep) (Quiver.Path.reverse p ≫ Quiver.Path.reverse (Quiver.Path.reverse p)) =
    Quot.mk (Quotient.CompClosure redStep) (𝟙 Y)
apply congr_comp_reverse