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