V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v' w' : V
p : Walk G v' w'
h : Adj G u v'
⊢ cons h (Walk.copy p (_ : v' = v') (_ : w' = w')) = Walk.copy (cons (_ : Adj G u v') p) (_ : u = u) (_ : w' = w')
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v w v' w' : V
h : Adj G u v
p : Walk G v' w'
hv : v' = v
hw : w' = w
⊢ cons h (Walk.copy p hv hw) = Walk.copy (cons (_ : Adj G u v') p) (_ : u = u) hw
subst_vars
no goals
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v' w' : V
p : Walk G v' w'
h : Adj G u v'
⊢ cons h (Walk.copy p (_ : v' = v') (_ : w' = w')) = Walk.copy (cons (_ : Adj G u v') p) (_ : u = u) (_ : w' = w')
rfl