Logipedia-Jumb

sigma_pi.exp_pi_l

exp.sym_eq_exp_body_S

exp.sym_eq_exp

logic.eq_f

nat.sym_eq_match_nat_type_S

bool.notb

nat.eq_minus

nat.sym_eq_eqb_body_S

nat.transitive_le

nat.not_le_Sn_O