hol - 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``)