DISP	Var_df	Var== Var
ABS	Var	Var == Atom
THM	Var_wf	Var
THM	Var_inc_atom	Var Atom
THM	discrete__Var	Discrete{Var}
THM	decidable__equal_Var	u,v:Var. Dec(u = v)

the other theories