Theorem: SimpleGraph.Walk.init₀_prefix (Untitled/Graphs/Walk.lean)

State before:
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
p' : Walk G a c
h : support p' <+: support p
⊢ init₀ p' <+: init₀ p
Tactic:
simpa [init_eq_take_support] using init_prefix h
State after:
no goals