# Generated by tools/translator: qualified upstream name -> MoonBit name.
ANTICHAIN antichain_v1
ANTICHAIN_SUBSET antichain_subset
CHAIN chain_v1
CHAIN_SUBSET chain_subset
DICKSON dickson
EXTEND_FLD extend_fld
EXTEND_INSEG extend_inseg
EXTEND_LINSEG extend_linseg
FINITE_FLD finite_fld
FLD_EQ_EMPTY fld_eq_empty
FLD_POINTWISE fld_pointwise
FLD_RESTRICT fld_restrict
FLD_RESTRICTED_SUBSET fld_restricted_subset
FLD_RESTRICT_POSET fld_restrict_poset
FLD_RESTRICT_QOSET fld_restrict_qoset
FLD_RESTRICT_TOSET fld_restrict_toset
FLD_RESTRICT_WOSET fld_restrict_woset
FLD_RESTRICT_WQOSET fld_restrict_wqoset
FLD_SUBSET fld_subset
FLD_SUC fld_suc
FLD_TRIVIAL fld_trivial
FLD_num fld_num
HP hp
INSEG_ANTISYM inseg_antisym
INSEG_FLD_SUBSET inseg_fld_subset
INSEG_LINSEG inseg_linseg
INSEG_ORDINAL inseg_ordinal
INSEG_PROPER_SUBSET inseg_proper_subset
INSEG_PROPER_SUBSET_FLD inseg_proper_subset_fld
INSEG_REFL inseg_refl
INSEG_SUBSET inseg_subset
INSEG_SUBSET_FLD inseg_subset_fld
INSEG_TRANS inseg_trans
INSEG_WOSET inseg_woset
IN_FLD in_fld
KL kl
KL_POSET_LEMMA kl_poset_lemma
LINSEG_FLD linseg_fld
LINSEG_INSEG linseg_inseg
LINSEG_WOSET linseg_woset
OEP oep
ORDINAL_CHAINED ordinal_chained
ORDINAL_CHAINED_LEMMA ordinal_chained_lemma
ORDINAL_FLD_SUBSET ordinal_fld_subset
ORDINAL_FLD_SUBSET_EQ ordinal_fld_subset_eq
ORDINAL_FLD_UNIQUE ordinal_fld_unique
ORDINAL_IMP_WOSET ordinal_imp_woset
ORDINAL_SUC ordinal_suc
ORDINAL_UNION ordinal_union
ORDINAL_UNION_LEMMA ordinal_union_lemma
ORDINAL_UP ordinal_up
PAIRED_EXT paired_ext
PBETA_TAC pbeta_tac
POSET_ANTISYM poset_antisym
POSET_FLDEQ poset_fldeq
POSET_IMP_QOSET poset_imp_qoset
POSET_MAX poset_max
POSET_MIN poset_min
POSET_QOSET poset_qoset
POSET_REFL poset_refl
POSET_RESTRICT poset_restrict
POSET_RESTRICTED_SUBSET poset_restricted_subset
POSET_TRANS poset_trans
POSET_TRIVIAL poset_trivial
POSET_num poset_num
PROPERLY_EQ_STRICTLY properly_eq_strictly
PROPERLY_MONO properly_mono
PROPERLY_PROPERLY properly_properly
PROPERLY_STRICTLY properly_strictly
QOSET_FLD qoset_fld
QOSET_FLDEQ qoset_fldeq
QOSET_MAX qoset_max
QOSET_MIN qoset_min
QOSET_POINTWISE qoset_pointwise
QOSET_REFL qoset_refl
QOSET_REFL_EQ qoset_refl_eq
QOSET_RESTRICT qoset_restrict
QOSET_TRANS qoset_trans
QOSET_TRIVIAL qoset_trivial
QOSET_num qoset_num
STRICTLY_EQ_PROPERLY strictly_eq_properly
STRICTLY_IMP_PROPERLY strictly_imp_properly
STRICTLY_PROPERLY strictly_properly
STRICTLY_STRICTLY strictly_strictly
SUBSET_PRED subset_pred
SUBWOSET_ISO_INSEG subwoset_iso_inseg
TOSET toset_v1
TOSET_COFINAL_WOSET toset_cofinal_woset
TOSET_IMP_POSET toset_imp_poset
TOSET_IMP_QOSET toset_imp_qoset
TOSET_MAX toset_max
TOSET_MIN toset_min
TOSET_POSET toset_poset
TOSET_RESTRICT toset_restrict
TOSET_TRIVIAL toset_trivial
TOSET_num toset_num
TUKEY tukey
UNIONS_PRED unions_pred
UNION_FLD union_fld
UNION_INSEG union_inseg
WF_INSEG_WOSET wf_inseg_woset
WO wo
WOSET woset_v1
WOSET_ANTISYM woset_antisym
WOSET_FINITE_TOSET woset_finite_toset
WOSET_FLDEQ woset_fldeq
WOSET_IMP_POSET woset_imp_poset
WOSET_IMP_QOSET woset_imp_qoset
WOSET_IMP_TOSET woset_imp_toset
WOSET_IMP_WQOSET woset_imp_wqoset
WOSET_INSEG_ORDINAL woset_inseg_ordinal
WOSET_POSET woset_poset
WOSET_REFL woset_refl
WOSET_RESTRICT woset_restrict
WOSET_TOSET woset_toset
WOSET_TOTAL woset_total
WOSET_TOTAL_LE woset_total_le
WOSET_TOTAL_LT woset_total_lt
WOSET_TRANS woset_trans
WOSET_TRANS_LE woset_trans_le
WOSET_TRANS_LESS woset_trans_less
WOSET_TRIVIAL woset_trivial
WOSET_WELL woset_well
WOSET_WELL_CONTRAPOS woset_well_contrapos
WOSET_WF woset_wf
WOSET_WQOSET woset_wqoset
WOSET_num woset_num
WO_ORDINAL wo_ordinal
WQOSET wqoset_v1
WQOSET_ANTICHAIN wqoset_antichain
WQOSET_IMP_QOSET wqoset_imp_qoset
WQOSET_IMP_WF wqoset_imp_wf
WQOSET_NOBAD wqoset_nobad
WQOSET_NOBAD_SUBSEQ wqoset_nobad_subseq
WQOSET_POINTWISE wqoset_pointwise
WQOSET_QOSET wqoset_qoset
WQOSET_RESTRICT wqoset_restrict
WQOSET_SUPERSET wqoset_superset
WQOSET_TRIVIAL wqoset_trivial
WQOSET_WF_SUPERSET wqoset_wf_superset
WQOSET_WF_SUPERSET_EQ wqoset_wf_superset_eq
WQOSET_num wqoset_num
ZL zl
ZL_STRONG zl_strong
ZL_SUBSETS zl_subsets
ZL_SUBSETS_UNIONS zl_subsets_unions
ZL_SUBSETS_UNIONS_NONEMPTY zl_subsets_unions_nonempty
antichain antichain
chain chain
fld fld
inseg inseg
linseg linseg
ordinal ordinal
poset poset
properly properly
qoset qoset
strictly strictly
toset toset
woset woset
wqoset wqoset
