(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
3
1.
a
: Atom
2.
b
: Atom
3.
a
=
b
inl(
*
)
(
a
=
b
a
=
b
)
By:
MemberEqCD
Generated subgoals:
1
*
(
a
=
b
)
1
step
2
(
a
=
b
)
Type
Auto
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(12steps total)
PrintForm
Definitions
core
StandardLIB
Doc
inl(*) 
(a = b 
a = b)
