blob: 3c0880b20c89544d88fa42e5c0162d55dfb65f85 (
plain)
1
2
3
4
5
6
7
8
9
10
|
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)
|
