Theorem: Path.snoc_cons (Complexes/Structures/Quiver.lean)

State before:
V : Sort u_1
inst✝ : Quiver V
A B C D : V
e : A ⟶ B
p : Path B C
e' : C ⟶ D
⊢ snoc (cons e p) e' = cons e (snoc p e')
Tactic:
cases p <;> simp
State after:
no goals