(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.
a
: Atom
2.
b
: Atom
a
=
b
a
=
b
By:
UseWitness if
a
=
b
Atom
inl(
*
); inr(
x
.
x
) fi
Generated subgoal:
1
if
a
=
b
Atom
inl(
*
); inr(
x
.
x
) fi
(
a
=
b
a
=
b
)
10
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 
a = b a = b a = b
Atom
inl(*); inr(
x.x) fi if a=bAtominl(*); inr(x.x) fi (a = b a = b)
