(17steps total)
PrintForm
Definitions
quot
1
Sections
StandardLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
dec
iff
ex
bvfun
2
1.
T
: Type
2.
E
:
T
T
Prop
3.
f
:(
T
T
).
x
,
y
:
T
.
f
(
x
,
y
)
E
(
x
,
y
)
4.
x
:
T
5.
y
:
T
Dec(
E
(
x
,
y
))
By:
Analyze 3
Generated subgoal:
1
3.
f
:
T
T
4.
x
,
y
:
T
.
f
(
x
,
y
)
E
(
x
,
y
)
5.
x
:
T
6.
y
:
T
Dec(
E
(
x
,
y
))
2
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(17steps total)
PrintForm
Definitions
quot
1
Sections
StandardLIB
Doc
T
f:(T
). 
x,y:T. f(x,y) 
E(x,y)
Dec(E(x,y))
