Доказательство теоремы HOL: добавление к существующей теории

Question

Я пытаюсь добавить теорему к существующей теории.Теорема, которую я пытаюсь добавить:

!l1 l2.LENGTH (APP l1 l2) = LENGTH l1 + l2  

Мой первый шаг - доказать теорему;однако, когда я пытаюсь установить цель, я получаю несколько сообщений об ошибках:

set_goal( [],``! (l1:'a list) (l2:'a list).LENGTH (APP l1 l2) = LENGTH l1 + l2``)`

Answer 1

Я думаю, что должно быть

∀l1 l2. LENGTH (APP l1 l2) = LENGTH l1 + LENGTH l2

и

set_goal([], ``! (l1:'a list) (l2:'a list).LENGTH (APP l1 l2) = LENGTH l1 + LENGTH l2``)