index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
test-suite
/
output
/
Search_bug13298.v
blob: 9a75321c645d647de42aa6074d06fb6e205afbcd (
plain
)
1
2
3
Set
Primitive
Projections
.
Record
c
:
Type
:=
{
fst
:
nat
;
snd
:
fst
=
0
}.
Search
concl:
fst
.
