simp only [rotate, tail_support_append]
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v : V
c : Walk G v v
h : u ∈ support c
⊢ List.tail (support (rotate c h)) ~r List.tail (support c)
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v : V
c : Walk G v v
h : u ∈ support c
⊢ (List.tail (support (dropUntil c u h)) ++ List.tail (support (takeUntil c u h))) ~r List.tail (support c)