1signature countableLib = sig
2  include Abbrev
3  val mk_count_aux_inj_rwt_ttac : hol_type list -> tactic option -> thm list
4  val mk_count_aux_inj_rwt : hol_type list -> thm list
5  val inj_rwt_to_countable : thm -> thm
6end
7