index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
test-suite
/
failure
/
Case5.v
blob: bdb5544bbaa3c294f8776c9c97bc56cbd0ea91e1 (
plain
)
1
2
3
Inductive
MS:
Set
:=
X:
MS
->
MS
|
Y:
MS
->
MS
.
Type
[
p:
MS
]
<
nat
>
Cases
p
of
(
X
x
)
=>
O
end
.
