cases xs
α : Type u_1
n : Nat
xs : ListN α n
⊢ xs.append nil ≅ xs
case mk
α : Type u_1
n : Nat
toList✝ : List α
length_eq✝ : toList✝.length = n
⊢ { toList := toList✝, length_eq := length_eq✝ }.append nil ≅ { toList := toList✝, length_eq := length_eq✝ }