# Generated by tools/translator: qualified upstream name -> MoonBit name.
define_quotient_type define_quotient_type
lift_function lift_function
lift_theorem lift_theorem
