(6steps total)
PrintForm
Definitions
Lemmas
DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
card
nsub0
union
A
:Type. (
0+
A
) ~
A
By:
Auto
Generated subgoal:
1
1.
A
: Type
(
0+
A
) ~
A
5
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(6steps total)
PrintForm
Definitions
Lemmas
DiscreteMath
Sections
DiscrMathExt
Doc
A:Type. (
0+A) ~ A
(0+A) ~ A
