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


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 2. reflexivity.
Qed.