test-suite/bugs/closed/4480.v


1
2
3
4
5
6
7
8
9
10
11
12

Require Import Setoid.

Definition proj (P Q : Prop) := P.

Lemma foo (P : Prop) : proj P P = P.
Admitted.
Lemma trueI : True <-> True.
Admitted.
Goal True.
  Fail setoid_rewrite foo.
  Fail setoid_rewrite trueI.