summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/1425.v
blob: 6be30174ae992f1799ba655aa33cd41885ceff58 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
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.