TheoremsantisymmRel_congr, antisymmRel_congr_left, antisymmRel_congr_right, eq, ge, image, le, le_congr, le_congr_left, le_congr_right, lt_congr, lt_congr_left, lt_congr_right, not_gt, not_lt, of_eq, refl, rfl, setoid_r, symmGen, symmGen_congr, symmGen_congr_left, symmGen_congr_right, trans, trans_le, trans_lt, trans_symmGen, ind, induction_on, prodEquiv_apply_mk, prodEquiv_symm_apply_mk, antisymmRel, lt_or_antisymmRel, trans_antisymmRel, not_antisymmRel, not_antisymmRel_symm, symmGen, symmGen_symm, trans_antisymmRel, left, right, ofAntisymmetrization_apply, antisymmetrization_apply, antisymmetrization_apply_mk, coe_antisymmetrization, dualAntisymmetrization_apply, dualAntisymmetrization_symm_apply, of_antisymmRel_of_symmGen, of_gt, of_lt, of_symmGen_of_antisymmRel, trans_antisymmRel, acc_antisymmetrization_iff, antisymmRel_comm, antisymmRel_iff_eq, antisymmRel_swap, antisymmRel_swap_apply, antisymmetrization_fibration, instIsTransAntisymmRel, instReflAntisymmRel, instSubsingletonAntisymmetrization, instSymmAntisymmRel, instWellFoundedGTAntisymmetrizationLe, instWellFoundedLTAntisymmetrizationLe, le_iff_lt_or_antisymmRel, le_of_antisymmRel_of_le, le_of_le_of_antisymmRel, lt_of_antisymmRel_of_lt, lt_of_lt_of_antisymmRel, not_antisymmRel_of_gt, not_antisymmRel_of_lt, not_gt_of_antisymmRel, not_lt_of_antisymmRel, ofAntisymmetrization_le_ofAntisymmetrization_iff, ofAntisymmetrization_lt_ofAntisymmetrization_iff, toAntisymmetrization_le_toAntisymmetrization_iff, toAntisymmetrization_lt_toAntisymmetrization_iff, toAntisymmetrization_mono, toAntisymmetrization_ofAntisymmetrization, wellFoundedGT_antisymmetrization_iff, wellFoundedLT_antisymmetrization_iff, wellFounded_antisymmetrization_iff | 82 |