summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/1604.v
blob: 22c3df824b0aadb9db24e7c6c78b9c3da17823ec (plain)
1
2
3
4
5
6
7
Require Import Setoid.

Parameter F : nat -> nat.
Axiom F_id : forall n : nat, n = F n.
Goal forall n : nat, F n = n.
intro n. setoid_rewrite F_id at 3. reflexivity.
Qed.