While trying to prove some equality in ssreflect, I got to the following:
WTS: forall (a b: ~ false), a = b
which is basically
WTS: forall (a b: false <> true), a = b.
Knowing that the following holds constructively,
bool_irrelevance (b: bool): (x y: b), x = y
I got to wonder if it is possible to prove WTS constructively.
Since the decidable equality required for is given as {x = y} + {x <> y}, I think it might be provable without axioms. Is this provable?
Also, is it possible to prove proof irrelevance for the prop False -> False?
Note, I am indeed fine with using proof irrelevance axiom. Simply asking if there is a way to avoid using the axiom.