is mentioned by

Thm* F,F':Formula. Dec(F = F')	[decidable__equal_Formula]
Thm* Discrete{Formula}	[discrete__Formula__with_rank]
Thm* Discrete{Formula}	[discrete__Formula]

In prior sections: formula formula rank

Try larger context: ClassicalProps(jlc)