aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/shouldsucceed/1243.v
blob: 7d6781db27a7b8652f11a05391fbf04889d78b28 (plain)
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.