Logipedia-Jumb

nat.eq_match_nat_type_O

nat.injective_plus_r

nat.plus_n_Sm

connectives.Not_ind

bool.match_bool_type

nat.le_n_Sn

bigops.sub_lt

nat.lt_O_S

nat.eq_minus_body_S

connectives.equal_leibniz