(9steps total)
PrintForm
Definitions
Lemmas
DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
card
nat
vs
nat
tuples
all
1
4
(
k
:{
k
:
|
0 =
k
}
k
) ~ (
k
:
k
)
By:
OOCifExteq THEN Analyze
Generated subgoal:
1
1.
x
:
k
:{
k
:
|
0 =
k
}
k
x
k
:
k
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(9steps total)
PrintForm
Definitions
Lemmas
DiscreteMath
Sections
DiscrMathExt
Doc
(k:{k:
| 
0 = k 
}
k
) ~ (k:
k) (k:{k:| 0 = k }k) ~ (k:k)| 0 = k }k
x k:k
