小编use*_*846的帖子

我想在一个名为理论的理论中定义我自己的列表类型List,但是已经存在一个具有该名称的理论.是否有比它更轻量级的理论Main？

所以我在子目标中有一个错误的假设.它是不同构造函数之间的相等.我如何完成子目标？

H: List.Not_Empty Bit.Bit Bit.Zero (List.Empty Bit.Bit) = List.Empty Bit.Bit