summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/shouldsucceed/1425.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/bugs/closed/shouldsucceed/1425.v')
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1425.v19
1 files changed, 0 insertions, 19 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/1425.v b/test-suite/bugs/closed/shouldsucceed/1425.v
deleted file mode 100644
index 6be30174..00000000
--- a/test-suite/bugs/closed/shouldsucceed/1425.v
+++ /dev/null
@@ -1,19 +0,0 @@
-Require Import Setoid.
-
-Parameter recursion : forall A : Set, A -> (nat -> A -> A) -> nat -> A.
-
-Axiom recursion_S :
- forall (A : Set) (EA : relation A) (a : A) (f : nat -> A -> A) (n : nat),
- EA (recursion A a f (S n)) (f n (recursion A a f n)).
-
-Goal forall n : nat, recursion nat 0 (fun _ _ => 1) (S n) = 1.
-intro n.
-rewrite recursion_S.
-reflexivity.
-Qed.
-
-Goal forall n : nat, recursion nat 0 (fun _ _ => 1) (S n) = 1.
-intro n.
-setoid_rewrite recursion_S.
-reflexivity.
-Qed. \ No newline at end of file