theory Vars imports Nominal2.Nominal2 begin text ‹ The type of variables is abstract and provided by the Nominal package. All we know is that it is countable. › atom_decl var end