index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
test-suite
/
output
/
SearchRewrite.out
blob: f87aea1c8444b93675a1c888060e349357e68d03 (
plain
)
1
2
plus_n_O: forall n : nat, n = n + 0 plus_O_n: forall n : nat, 0 + n = n