rw [Path.inverse_snoc]
V : Sort u_1
inst✝ : SerreGraph V
A B✝ : V
e : A ⟶ B✝
p : Path B✝ A
⊢ next (next A (Path.cons' A B✝ A e p)) (Path.inverse (Path.snoc p e)) = A
V : Sort u_1
inst✝ : SerreGraph V
A B✝ : V
e : A ⟶ B✝
p : Path B✝ A
⊢ next (next A (Path.cons' A B✝ A e p)) (Path.cons (SerreGraph.op e) (Path.inverse p)) = A