index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
test-suite
/
bugs
/
opened
/
3417.v
blob: 355fd17ff93d6764310dbe6d661ead8b5553a1e1 (
plain
)
1
2
3
Goal
forall
{
T
}(
a
b
:
T
),
b
=
a
->
{
c
|
c
=
b
}.
intros
T
a
b
H
.
Fail
setoid_rewrite
H
.
