# Generated by tools/translator: qualified upstream name -> MoonBit name.
BIT0_DEF bit0_def
BIT1_DEF bit1_def
INDUCT_TAC induct_tac
IND_SUC_0 ind_suc_0
IND_SUC_0_EXISTS ind_suc_0_exists
IND_SUC_INJ ind_suc_inj
IND_SUC_SPEC ind_suc_spec
INFINITY_AX infinity_ax
NOT_SUC not_suc
NUMERAL numeral
NUM_REP_CASES num_rep_cases
NUM_REP_INDUCT num_rep_induct
NUM_REP_RULES num_rep_rules
ONE_ONE one_one
ONTO onto
SUC_DEF suc_def
SUC_INJ suc_inj
ZERO_DEF zero_def
dest_small_numeral dest_small_numeral
is_numeral is_numeral
mk_numeral mk_numeral
mk_small_numeral mk_small_numeral
new_specification new_specification
num_Axiom num_axiom
num_CASES num_cases
num_INDUCTION num_induction
num_RECURSION num_recursion
num_tydef num_tydef
the_specifications the_specifications
