Logipedia-Jumb

bigops.sym_eq_bigop_body_S

div_mod.axiom_div_aux_body_S

nat.sym_eq_times_body_O

primes.dividesb

exp.sym_eq_exp_body_S

nat.eq_times_body_O

bool.eq_match_bool_type_true

nat.axiom_times

nat.sym_eq_match_nat_type_O

permutation.axiom_invert_permut