simp only [ListN.append]
case mk.a
α : Type u_1
n : Nat
toList✝ : List α
length_eq✝ : toList✝.length = n
⊢ ({ toList := toList✝, length_eq := length_eq✝ }.append nil).toList ≅
    { toList := toList✝, length_eq := length_eq✝ }.toList
case mk.a
α : Type u_1
n : Nat
toList✝ : List α
length_eq✝ : toList✝.length = n
⊢ toList✝ ++ [] ≅ toList✝