# Generated by tools/translator: qualified upstream name -> MoonBit name.
ETA_ONE eta_one
EXISTS_ONE_REP exists_one_rep
EXISTS_ONE_THM exists_one_thm
FORALL_ONE_THM forall_one_thm
I_DEF i_def
I_O_ID i_o_id
I_THM i_thm
o_ASSOC o_assoc
o_DEF o_def
o_THM o_thm
one one
one_Axiom one_axiom_v1
one_DEF one_def
one_INDUCT one_induct
one_RECURSION one_recursion
one_axiom one_axiom
one_tydef one_tydef
