(12steps total)
PrintForm
Definitions
core
StandardLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
decidable
atom
equal
1
1
4
1.
a
: Atom
2.
b
: Atom
3.
a
=
b
inr(
x
.
x
)
(
a
=
b
a
=
b
)
By:
Auto
Generated subgoal:
1
(
x
.
x
)
(
a
=
b
)
3
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(12steps total)
PrintForm
Definitions
core
StandardLIB
Doc
a = b
inr(
x.x) 
(a = b 
