(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
1
1.
A
: Type
(
0+
A
) ~
A
By:
Rewrite by (
0+
A
) ~ ({
x
:
A
| False }+{
x
:
A
|
False })
Generated subgoals:
1
(
0+
A
) ~ ({
x
:
A
| False }+{
x
:
A
|
False })
3
steps
2
({
x
:
A
| False }+{
x
:
A
|
False }) ~
A
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(6steps total)
PrintForm
Definitions
Lemmas
DiscreteMath
Sections
DiscrMathExt
Doc
(
0+A) ~ A (0+A) ~ A0+A) ~ ({x:A| False }+{x:A| 
False }) (0+A) ~ ({x:A| False }+{x:A| False })
({x:A| False }+{x:A| False }) ~ A
