Theorem: LoVe.Vec.meld_append (LoVe/Labs/Lab4Solution.lean)

State before:
α β γ : Type
m n : ℕ
f : α → β → γ
xs : Vec α m
ys : Vec β m
⊢ meld f (append V[] xs) (append V[] ys) = append (meld f V[] V[]) (meld f xs ys)
Tactic:
simp [append, meld]
State after:
no goals

State before:
α β γ : 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))
Tactic:
rw [ih]
State after:
no goals