Доказательство того, что конкатенация языков ассоциативна в Agda

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

У меня возникают проблемы с доказательством ассоциативности конкатенации языков. Доказательство будет выделено желтым цветом, поскольку Agda не смогла найти слова для "++ Assoc" в следующем коде:

LangAssoc : ∀{Σ}{l1 l2 l3 : Language Σ}{w : Word Σ} → (LangConc l1 (LangConc l2 l3)) w → (LangConc (LangConc l1 l2) l3) w
LangAssoc {l1 = l1} (conc x (conc y z)) = conc (conc (subst l1 (++Assoc _ _ _) x) y) z

Где "++ Assoc" - это доказательство ассоциативности объединения списков.

Язык и конкатенация определяются следующим образом:

Language : ℕ → Set₁
Language a = Word a → Set

data LangConc {Σ} (l1 l2 : Language Σ) : Language Σ where
  conc : ∀{w1 w2} → l1 w1 → l2 w2 → (LangConc l1 l2) (w1 ++ w2)

Поэтому я хотел бы спросить, может ли кто-нибудь объяснить, что я делаю не так в этой ситуации, и дать мне несколько подсказок о том, как решить эту проблему.

Изменить 1: я пробовал другой способ, используя подстановку вне конкатенации, но я застрял в этой ситуации:

LangAssoc : ∀{Σ} {l1 l2 l3 : Language Σ} {w : Word Σ} → (LangConc l1 (LangConc l2 l3)) w → (LangConc (LangConc l1 l2) l3) w
LangAssoc {Σ} {l1 = l1} {l2 = l2} {l3 = l3} (conc x (conc y z)) = subst {!!} (++Assoc {Σ} _ _ _) (conc {Σ} (conc {Σ} x y) z)

Изменить 2: я только что попробовал использовать следующий код и получил сообщение об ошибке.

LangAssoc : ∀{Σ} {l1 l2 l3 : Language Σ} {w : Word Σ} → (LangConc l1 (LangConc l2 l3)) w → (LangConc (LangConc l1 l2) l3) w
LangAssoc {l1 = l1} {w = w} (conc x (conc y z)) =  ?

w1 ++ w2 != w of type List (Fin Σ)
when checking that the pattern conc x (conc y z) has type
LangConc l1 (LangConc l2 l3) w

Изменить 3: просто была еще одна попытка, разбив слово w на три части, как было предложено.

LangAssoc : ∀{Σ : ℕ}{l1 l2 l3 : Language Σ}{w1 w2 w3 : Word Σ} 
             → (LangConc l1 (LangConc l2 l3)) (w1 ++ w2 ++ w3)
             → (LangConc (LangConc l1 l2) l3) ((w1 ++ w2) ++ w3)
LangAssoc (conc {w1} x (conc {w2} {w3} y z))
   = subst (LangConc (LangConc _ _) _) (++Assoc w1 w2 w3) (conc (conc x y) z)

Сообщение об ошибке:

w4 != w1 of type List (Fin Σ)
when checking that the pattern conc {w1} x (conc {w2} {w3} y z) has
type LangConc l1 (LangConc l2 l3) (w1 ++ w2 ++ w3)

где List (Fin Σ) - определение слова Σ.