# Generated by tools/translator: qualified upstream name -> MoonBit name.
ABS_SIMP abs_simp
AC ac
AND_CLAUSES and_clauses
AND_FORALL_THM and_forall_thm
BETA_THM beta_thm
CLAIM_TAC claim_tac
CONJ_ACI conj_aci
CONJ_ASSOC conj_assoc
CONJ_SYM conj_sym
DESTRUCT_TAC destruct_tac
DISJ_ACI disj_aci
DISJ_ASSOC disj_assoc
DISJ_SYM disj_sym
EQ_CLAUSES eq_clauses
EQ_IMP eq_imp
EQ_REFL eq_refl
EQ_SYM eq_sym
EQ_SYM_EQ eq_sym_eq
EQ_TRANS eq_trans
EXISTS_OR_THM exists_or_thm
EXISTS_REFL exists_refl
EXISTS_SIMP exists_simp
EXISTS_UNIQUE exists_unique
EXISTS_UNIQUE_ALT exists_unique_alt
EXISTS_UNIQUE_REFL exists_unique_refl
EXISTS_UNIQUE_THM exists_unique_thm
FIX_TAC fix_tac
FORALL_AND_THM forall_and_thm
FORALL_SIMP forall_simp
FORALL_UNWIND_THM1 forall_unwind_thm1
FORALL_UNWIND_THM2 forall_unwind_thm2
HYP_TAC hyp_tac
IMP_CLAUSES imp_clauses
IMP_CONJ imp_conj
IMP_CONJ_ALT imp_conj_alt
IMP_IMP imp_imp
INTRO_TAC intro_tac
LEFT_AND_EXISTS_THM left_and_exists_thm
LEFT_AND_FORALL_THM left_and_forall_thm
LEFT_EXISTS_AND_THM left_exists_and_thm
LEFT_FORALL_IMP_THM left_forall_imp_thm
LEFT_IMP_EXISTS_THM left_imp_exists_thm
LEFT_OR_DISTRIB left_or_distrib
LEFT_OR_EXISTS_THM left_or_exists_thm
MONO_AND mono_and
MONO_EXISTS mono_exists
MONO_FORALL mono_forall
MONO_IMP mono_imp
MONO_NOT mono_not
MONO_OR mono_or
NOT_CLAUSES_WEAK not_clauses_weak
OR_CLAUSES or_clauses
OR_EXISTS_THM or_exists_thm
REFL_CLAUSE refl_clause
RIGHT_AND_EXISTS_THM right_and_exists_thm
RIGHT_AND_FORALL_THM right_and_forall_thm
RIGHT_EXISTS_AND_THM right_exists_and_thm
RIGHT_FORALL_IMP_THM right_forall_imp_thm
RIGHT_IMP_FORALL_THM right_imp_forall_thm
RIGHT_OR_DISTRIB right_or_distrib
RIGHT_OR_EXISTS_THM right_or_exists_thm
SWAP_EXISTS_THM swap_exists_thm
SWAP_FORALL_THM swap_forall_thm
TRIV_AND_EXISTS_THM triv_and_exists_thm
TRIV_EXISTS_AND_THM triv_exists_and_thm
TRIV_EXISTS_IMP_THM triv_exists_imp_thm
TRIV_FORALL_IMP_THM triv_forall_imp_thm
TRIV_FORALL_OR_THM triv_forall_or_thm
TRIV_OR_FORALL_THM triv_or_forall_thm
UNWIND_THM1 unwind_thm1
UNWIND_THM2 unwind_thm2
WLOG_RELATION wlog_relation
