signature countable_typesLib = sig include Abbrev val mk_countable : hol_type -> thm end
HOL 4, Trindemossen-1