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