Показ (голова. init), = направляются в Agda

Я пытаюсь доказать простую лемму в Agda, который я думаю, верно.

Если вектор имеет больше чем два элемента, беря head следующее взятие init совпадает со взятием head сразу.

Я сформулировал его следующим образом:

lem-headInit : ∀{l} (xs : Vec ℕ (suc (suc l)))
                    -> head (init xs) ≡ head xs
lem-headInit (x ∷ xs) = ?

Который дает мне;

.l : ℕ
x  : ℕ
xs : Vec ℕ (suc .l)
------------------------------
Goal: head (init (x ∷ xs) | (initLast (x ∷ xs) | initLast xs)) ≡ x

как ответ.

Я действительно не полностью понимаю, как читать (init (x ∷ xs) | (initLast (x ∷ xs) | initLast xs)) компонент. Я предполагаю, что мои вопросы; действительно ли возможно, как и что это называет средним.

Большое спасибо.