其实只有一颗，但是每个 definition 会同时有对应的 case tree 和 clauses。所谓的存进 signature 的东西其实只是 definition 的另一种写法而已，为了方便写后面的 inference rules。