rw [ih]
α β γ : Type
m n : ℕ
f : α → β → γ
v : α
n✝ : ℕ
vs : Vec α n✝
w : β
ws : Vec β n✝
xs : Vec α m
ys : Vec β m
ih : meld f (append vs xs) (append ws ys) = append (meld f vs ws) (meld f xs ys)
⊢ cons (f v w) (meld f (append vs xs) (append ws ys)) = cons (f v w) (append (meld f vs ws) (meld f xs ys))
no goals