Agda 列表是与 1 的列表连接起来的天然通用列表的最后一个

问：

我有这个功能：

natListLast : List ℕ → ℕ
natListLast []            = 0
natListLast nats@(x ∷ xs) = v.last (v.fromList nats)

当我这样做时

_ : natListLast (2 l.∷ l.[] l.++ 1 l.∷ l.[]) ≡ 1
_ = refl

我没有收到任何错误。

但是当我试图将其推广到这样的任意内容时：List nat

natListConcatLast : (nats : List ℕ) → natListLast (nats l.++ 1 l.∷ l.[]) ≡ 1
natListConcatLast [] = refl
natListConcatLast nats@(x ∷ xs) = ?

我不确定该用什么替换。?

我试着从以下几个方面开始：begin

natListConcatLast : (nats : List ℕ) → natListLast (nats l.++ 1 l.∷ l.[]) ≡ 1
natListConcatLast [] = refl
natListConcatLast nats@(x ∷ xs) =
  begin
    natListLast (nats l.++ 1 l.∷ l.[])
  ≡⟨⟩
    v.last (v.fromList ((x l.∷ xs) l.++ 1 l.∷ l.[]))
  ≡⟨⟩
    ?
  ≡⟨⟩
    1
  ∎

但是我收到此错误：

1 !=
(last (fromList ((x List.∷ xs) l.++ 1 List.∷ List.[]))
 | initLast (fromList ((x List.∷ xs) l.++ 1 List.∷ List.[])))
of type ℕ
when checking that the expression 1 ∎ has type
last (fromList ((x List.∷ xs) l.++ 1 List.∷ List.[])) ≡ 1

我不确定如何解释此错误。我不知道如何处理.| initLast

谢谢！