test-suite/bugs/closed/shouldsucceed/1243.v


1
2
3
4
5
6
7
8
9
10
11
12

Require Import ZArith.
Require Import Arith.
Open Scope Z_scope.

Theorem r_ex : (forall x y:nat, x + y = x + y)%nat.
Admitted.

Theorem r_ex' : forall x y:nat, (x + y = x + y)%nat.
Admitted.