(11steps total)
PrintForm
Definitions
Lemmas
DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
card
pi
vs
nsub
pi
1
1
1
1
1.
b
:
0
2.
y
:
i
:
0
b
(
i
)
(
x
.
x
) =
y
By:
FunExtensionality
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(11steps total)
PrintForm
Definitions
Lemmas
DiscreteMath
Sections
DiscrMathExt
Doc
0
0b(i)
(
x.x) = y
