let p' := p.inverse
V : Sort u_1
G : SerreGraph V
A B C : V
p✝ p : Path A B
⊢ 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
⊢ last p = first (inverse p)