have pinv : p = p'.inverse := by simp
V : Sort u_1
G : SerreGraph V
A B C : V
p✝ p : Path A B
p' : Path B A := inverse p
⊢ last p = first (inverse p)
V : Sort u_1
G : SerreGraph V
A B C : V
p✝ p : Path A B
p' : Path B A := inverse p
pinv : p = inverse p'
⊢ last p = first (inverse p)