case h
α : Type u_1
β : Type ?u.46498
n n' m : ℕ
s✝ : Sym α n
a b : α
s s' : Sym α n'
⊢ ↑(append s s') = ↑(↑(Sym.cast (_ : n' + n' = n' + n')) (append s' s))
α : Type u_1
β : Type ?u.46498
n n' m : ℕ
s✝ : Sym α n
a b : α
s s' : Sym α n'
⊢ append s s' = ↑(Sym.cast (_ : n' + n' = n' + n')) (append s' s)
ext
no goals
case h
α : Type u_1
β : Type ?u.46498
n n' m : ℕ
s✝ : Sym α n
a b : α
s s' : Sym α n'
⊢ ↑(append s s') = ↑(↑(Sym.cast (_ : n' + n' = n' + n')) (append s' s))
simp [append, add_comm]