bug_9180.out « output « test-suite - coq - The formal proof system

about summary refs log tree commit diff

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

blob: ed4892b3897e4c446b0563360a3ae9b33772ea74 (plain)

Notation
"n .+1" := S n : nat_scope (default interpretation)
forall x : nat, x.+1 = x.+1
     : Prop