Open problem: Prove ¬◇a => ⊥^a constructively or prove it is impossible to prove

[bvssvni]

Currently, the proof ¬◇a => ⊥^a requires a do be decidable, which means it only holds in classical logic. See modal::npos_to_para. This will be available in v0.27.

The problem is whether this is possible to do constructively or not.

This requires proving ¬◇a => ⊥^a constructively or ⊥^((¬◇a => ⊥^a)^⊤) constructively (or similar) in Prop.

[bvssvni]

Closed by #469

Conclusion: It is constructive.