case mk
α : Type u
β : Type v
φ : Type w
n✝ n m : ℕ
w : Vector α m
val✝ : List α
property✝ : List.length val✝ = n
⊢ toList (append { val := val✝, property := property✝ } w) = toList { val := val✝, property := property✝ } ++ toList w
α : Type u
β : Type v
φ : Type w
n✝ n m : ℕ
v : Vector α n
w : Vector α m
⊢ toList (append v w) = toList v ++ toList w
cases v
case mk.mk
α : Type u
β : Type v
φ : Type w
n✝ n m : ℕ
val✝¹ : List α
property✝¹ : List.length val✝¹ = n
val✝ : List α
property✝ : List.length val✝ = m
⊢ toList (append { val := val✝¹, property := property✝¹ } { val := val✝, property := property✝ }) =
    toList { val := val✝¹, property := property✝¹ } ++ toList { val := val✝, property := property✝ }
case mk
α : Type u
β : Type v
φ : Type w
n✝ n m : ℕ
w : Vector α m
val✝ : List α
property✝ : List.length val✝ = n
⊢ toList (append { val := val✝, property := property✝ } w) = toList { val := val✝, property := property✝ } ++ toList w
cases w
no goals
case mk.mk
α : Type u
β : Type v
φ : Type w
n✝ n m : ℕ
val✝¹ : List α
property✝¹ : List.length val✝¹ = n
val✝ : List α
property✝ : List.length val✝ = m
⊢ toList (append { val := val✝¹, property := property✝¹ } { val := val✝, property := property✝ }) =
    toList { val := val✝¹, property := property✝¹ } ++ toList { val := val✝, property := property✝ }
rfl