(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
1.
A
: Type
(
0+
A
) ~ ({
x
:
A
| False }+{
x
:
A
|
False })
By:
BackThru:
Thm*
(
A
~
A'
)
(
B
~
B'
)
((
A
+
B
) ~ (
A'
+
B'
)) THEN OOCifExteq
Generated subgoals:
1
0 =ext {
x
:
A
| False }
1
step
2
A
=ext {
x
:
A
|
False }
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) ~ ({x:A| False }+{x:A| 
False }) (0+A) ~ ({x:A| False }+{x:A| False })
(B ~ B') ((A+B) ~ (A'+B')) THEN OOCifExteq 0 =ext {x:A| False }
A =ext {x:A| False }
