(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
1.
T
: Type
2.
E
:
T
Prop
3.
x
:
T
. Dec(
E
(
x
))
4.
x
:
T
!
b
:
.
b
E
(
x
)
By:
FwdThru:
Thm*
Dec(
P
)
(
b
:
.
b
P
) on [ Dec(
E
(
x
)) ]
Generated subgoal:
1
5.
b
:
.
b
E
(
x
)
!
b
:
.
b
E
(
x
)
5
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))
!b:
. b 
E(x)
