(2steps 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
2
A
:Type. (
A
+
0) ~
A
By:
Rewrite by
Thm*
(
A
+
B
) ~ (
B
+
A
)
Generated subgoal:
1
1.
A
: Type
(
0+
A
) ~
A
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(2steps total)
PrintForm
Definitions
Lemmas
DiscreteMath
Sections
DiscrMathExt
Doc
A:Type. (A+
0) ~ A A:Type. (A+0) ~ A (0+A) ~ A
