(5steps total)
PrintForm
Definitions
core
StandardLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
iff
preserves
decidability
1
2
1.
A
: Prop
2.
B
: Prop
3.
A
4.
A
B
B
B
By:
(DNth 2 0) THEN (Analyze 0)
Generated subgoal:
1
4.
A
B
5.
A
B
6.
B
False
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(5steps total)
PrintForm
Definitions
core
StandardLIB
Doc