Logipedia-Jumb

nat.eqb_elim

permutation.invert_permut_f

permutation.sym_eq_invert_permut

nat.le_S_S_to_le

nat.le_to_not_lt

permutation.f_invert_permut

permutation.transpose_transpose

nat.commutative_plus

sigma_pi.exp_pi_bc

bool.match_bool_type