blob: 7358068c8dead6f10921b749ecb79312db9a501c (
plain)
1
2
3
4
5
6
7
8
9
|
From Coq Require Import ssreflect Setoid.
Structure SEProp := {prop_of : Prop; _ : prop_of <-> True}.
Fact anomaly: forall P : SEProp, prop_of P.
Proof.
move=> [P E].
Fail rewrite E.
Abort.
|