is mentioned by

Thm* Dec(True)

[decidable__true]

In prior sections: core discrete jlc bool 1