plus_n_O: forall n : nat, n = n + 0
(use "About" for full details on implicit arguments)
plus_O_n: forall n : nat, 0 + n = n
(use "About" for full details on implicit arguments)
h: n = newdef n
(use "About" for full details on implicit arguments)
h: n = newdef n
(use "About" for full details on implicit arguments)
h: n = newdef n
(use "About" for full details on implicit arguments)