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