Logipedia
Modules
About
FAQ
Search
Search
exp.axiom_exp_body_S
connectives.True
logic.eq_coerc
nat.le_n_O_elim
nat.eq_times_body_O
cong.congruent_n_n
nat.minus_to_plus
logic.not_to_not
nat.leb_elim
nat.eq_times