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