宇宙与sumbool不一致

Question

我已经定义并证明了以下引理：

    NM.In k m -> {NM.In k m0}+{NM.In k m1}.

我还可以证明一个对称引理：

    {NM.In k m0}+{NM.In k m1} -> NM.In k m

但是，当我尝试将它们合并为一个时：

    NM.In k m <-> {NM.In k m0}+{NM.In k m1}.

我收到以下错误：

The term "sumbool (@NM.In CarrierA k m0) (@NM.In CarrierA k m1)" has type 
"Set" while it is expected to have type "Prop" (universe inconsistency: Cannot enforce
Set = Prop).

这怎么可以解决？

Answer 1

正如丹尼尔指出的那样，问题在于<->结缔组织只把命题作为论据，而sumbool则生活在Set。这可以通过以下几种方式规避：你可以用sumbool替换or，或者你可以用计算相关的连接词取代iff：

Variables A B C : Prop.

Check (({A} + {B} -> C) * (C -> {A} + {B}))%type.