is mentioned by

Thm* u,v:Var. Dec(u = v)	[decidable__equal_Var]
Thm* Discrete{Var}	[discrete__Var]
Thm* Var Atom	[Var_inc_atom]

Try larger context: ClassicalProps(jlc)