blob: 08a86330f256d2dbadeb629194877fdfeb80aca6 (
plain)
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.
|