Logipedia-Jumb

nat.filter_nat_type

nat.sym_eq_leb_body_S

exp.sym_eq_exp_body_O

connectives.I

nat.axiom_leb_body_O

nat.lt_to_not_eq

permutation.transpose_i_j_i

connectives.match_And_prop

nat.distributive_times_plus_r

nat.associative_times