SearchRewrite.out « output « test-suite - coq - the Coq proof assistant

about summary refs log tree commit diff homepage

path: root/test-suite/output/SearchRewrite.out

blob: 5edea5dff6bb591d64849b7dbf14a526cdf778ee (plain)

plus_n_O: forall n : nat, n = n + 0
plus_O_n: forall n : nat, 0 + n = n
h: n = newdef n
h: n = newdef n
h: n = newdef n