доказать теорему в агде. Ошибка: должен быть тип функции, но не

Question

Вот теорема, которую я хочу доказать.

prob4 : ∀(w x y z : ℕ) → w * (x + y + z) ≡ z * w + x * w + w * y 
prob 4 = {!!} 

Это то, что я написал

open import Data.Nat 
open import Data.Nat.Properties.Simple 
open import Relation.Binary.PropositionalEquality 

prob4a : ∀ (w x y z : ℕ) → w * (x + y + z) ≡ w * x + w * y + w * z 
prob4a 0 x y z = refl 
prob4a (suc w) x y z rewrite prob4a w x y z 
      | +-assoc (x + y + z) (w * x) (w * y) (w * z) = ? 

Я создал новую теорему prob4a, чтобы организовать вывод в правильном порядке. И он может использовать теоремы в nat.thms.agda, чтобы это доказать.

и ошибка

x + y + z + w * x + w * y ≡ x + y + z + (w * x + w * y) должен быть типом функции, но это не при проверке, что (w * z) является действительным аргументом функции типа x + y + z + w * x + w * y ≡ x + y + z + (w * x + w * y)

так Что это означает? и как я могу исправить это, чтобы доказать работу?

Answer 1

+-assoc принимает только 3 аргумента, но вы передали ему 4 аргумента.

Agda жалуется, что тип равенства не является типом функции, потому что результат +-assoc, примененный к 3 аргументам, является типом равенства, но передача 4-го аргумента означает, что вы хотите, чтобы он был функцией.