在试图证明 ssreflect 中的一些相等性时，我得到了以下结果：
WTS: forall (a b: ~ false), a = b
这基本上是
WTS: forall (a b: false <> true), a = b.
知道以下内容具有建设性，
bool_irrelevance (b: bool): (x y: b), x = y
我想知道是否有可能WTS建设性地证明。由于 所需的可判定相等性为{x = y} + {x <> y}，我认为它可能无需公理即可证明。这是可以证明的吗？
此外，是否有可能证明与道具无关的证据False -> False？
请注意，我确实可以使用证明无关公理。简单地询问是否有办法避免使用公理。