# Generated by tools/translator: qualified upstream name -> MoonBit name.
EXISTS_EQUATION exists_equation
MONO_TAC mono_tac
RIGHT_BETAS right_betas
derive_nonschematic_inductive_relations derive_nonschematic_inductive_relations
derive_strong_induction derive_strong_induction
monotonicity_theorems monotonicity_theorems
new_inductive_definition new_inductive_definition
prove_inductive_relations_exist prove_inductive_relations_exist
prove_monotonicity_hyps prove_monotonicity_hyps
strip_ncomb strip_ncomb
the_inductive_definitions the_inductive_definitions
