case mk
α : Type u_1
β : Type ?u.13471
n n' m : ℕ
s : Sym α n
a✝ b a : α
val✝ : List α
property✝ : List.length val✝ = n
⊢ ofVector (a ::ᵥ { val := val✝, property := property✝ }) = a ::ₛ ofVector { val := val✝, property := property✝ }
α : Type u_1
β : Type ?u.13471
n n' m : ℕ
s : Sym α n
a✝ b a : α
v : Vector α n
⊢ ofVector (a ::ᵥ v) = a ::ₛ ofVector v
cases v
no goals
case mk
α : Type u_1
β : Type ?u.13471
n n' m : ℕ
s : Sym α n
a✝ b a : α
val✝ : List α
property✝ : List.length val✝ = n
⊢ ofVector (a ::ᵥ { val := val✝, property := property✝ }) = a ::ₛ ofVector { val := val✝, property := property✝ }
rfl