1signature fcpLib = 2sig 3 include Abbrev 4 5 val index_type : Arbnum.num -> hol_type 6 val index_to_num : hol_type -> Arbnum.num 7 8 val INDEX_CONV : conv 9 val DIMINDEX : Arbnum.num -> thm 10 val FINITE : Arbnum.num -> thm 11 val SIZE : Arbnum.num -> thm 12 val FCP_ss : simpLib.ssfrag 13 14 val inst_fcp_lengths : term -> term 15end 16