no goals
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v : V
p : Walk G u v
d : Dart G
h : d ∈ darts p
⊢ d.snd ∈ support p
simpa using p.reverse.dart_fst_mem_support_of_mem_darts (by simp [h] : d.symm ∈ p.reverse.darts)
no goals
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v : V
p : Walk G u v
d : Dart G
h : d ∈ darts p
⊢ Dart.symm d ∈ darts (reverse p)
simp [h]