# Generated by tools/translator: qualified upstream name -> MoonBit name.
CHOICE_PAIRED_THM choice_paired_thm
CHOICE_UNPAIR_THM choice_unpair_thm
COMMA_DEF comma_def
CURRY_DEF curry_def
EXISTS_CURRY exists_curry
EXISTS_PAIRED_THM exists_paired_thm
EXISTS_PAIR_FUN_THM exists_pair_fun_thm
EXISTS_PAIR_THM exists_pair_thm
EXISTS_SWAP_FUN_THM exists_swap_fun_thm
EXISTS_TRIPLED_THM exists_tripled_thm
EXISTS_UNCURRY exists_uncurry
EXISTS_UNPAIR_FUN_THM exists_unpair_fun_thm
EXISTS_UNPAIR_THM exists_unpair_thm
FORALL_CURRY forall_curry
FORALL_PAIRED_THM forall_paired_thm
FORALL_PAIR_FUN_THM forall_pair_fun_thm
FORALL_PAIR_THM forall_pair_thm
FORALL_TRIPLED_THM forall_tripled_thm
FORALL_UNCURRY forall_uncurry
FORALL_UNPAIR_FUN_THM forall_unpair_fun_thm
FORALL_UNPAIR_THM forall_unpair_thm
FST fst
FST_DEF fst_def
GABS_CONV gabs_conv
GABS_DEF gabs_def
GEN_BETA_CONV gen_beta_conv
GEQ_DEF geq_def
LAMBDA_PAIR lambda_pair
LAMBDA_PAIR_THM lambda_pair_thm
LAMBDA_TRIPLE lambda_triple
LAMBDA_TRIPLE_THM lambda_triple_thm
LET_DEF let_def
LET_END_DEF let_end_def
LET_TAC let_tac
PAIR pair
PAIRED_ETA_THM paired_eta_thm
PAIR_EQ pair_eq
PAIR_EXISTS_THM pair_exists_thm
PAIR_SURJECTIVE pair_surjective
PASSOC_DEF passoc_def
REP_ABS_PAIR rep_abs_pair
SND snd
SND_DEF snd_def
SUBLET_CONV sublet_conv
UNCURRY_DEF uncurry_def
_FUNCTION _function
_GUARDED_PATTERN _guarded_pattern
_MATCH _match
_SEQPATTERN _seqpattern
_UNGUARDED_PATTERN _unguarded_pattern
dest_pair dest_pair
is_pair is_pair
let_CONV let_conv
mk_pair mk_pair
mk_pair_def mk_pair_def
new_definition new_definition
pair_INDUCT pair_induct
pair_RECURSION pair_recursion
prod_tybij prod_tybij
the_definitions the_definitions
