(9steps total)
PrintForm
Definitions
Lemmas
LogicSupplement
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
dec
pred
iff
some
boolfun
1
1.
T
: Type
2.
E
:
T
Prop
3.
x
:
T
. Dec(
E
(
x
))
f
:(
T
).
x
:
T
.
f
(
x
)
E
(
x
)
By:
DescribeFun:
f
by
x
:
T
.
!
b
:
.
b
E
(
x
) THEN Witness:
f
Generated subgoal:
1
4.
x
:
T
!
b
:
.
b
E
(
x
)
6
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(9steps total)
PrintForm
Definitions
Lemmas
LogicSupplement
Sections
DiscrMathExt
Doc
Prop
x:T. Dec(E(x))
f:(T
). 
E(x)
