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