is mentioned by

Thm* x,y:. Dec(x = y)	[decidable__equal_Three]
Thm* 3 = 3	[Three_eq_contradiction_ext]
Thm* x:. True	[Three_ind_ext]

Try larger context: ClassicalProps(jlc)