dsimp [inverse, length]
V : Sort u_1
G : SerreGraph V
A✝ B✝² C : V
p : Path A✝ B✝²
A B✝¹ B B✝ : V
a✝ : A ⟶ B✝
p' : Path B✝ B
⊢ length (inverse (cons a✝ p')) = length (cons a✝ p')
V : Sort u_1
G : SerreGraph V
A✝ B✝² C : V
p : Path A✝ B✝²
A B✝¹ B B✝ : V
a✝ : A ⟶ B✝
p' : Path B✝ B
⊢ length (snoc (inverse p') (SerreGraph.op a✝)) = Nat.succ (length p')