(10steps total)
PrintForm
Definitions
Lemmas
DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
nonfin
eqv
unb
inf
iff
negnegelim
1
2
1
1.
A
:Type.
Finite(
A
)
Unbounded(
A
)
2.
D
:Type.
(
D
)
(
D
)
3.
P
: Prop
4.
A
:Type.
P
= (
A
)
P
P
By:
Analyze-1 THEN Rewrite by
P
= (
A
)
Generated subgoal:
1
4.
A
: Type
5.
P
= (
A
)
Prop
(
A
)
(
A
)
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(10steps total)
PrintForm
Definitions
Lemmas
DiscreteMath
Sections
DiscrMathExt
Doc
A:Type. 
Finite(A) 
Unbounded(A)
D) 
