(2steps total)
PrintForm
Definitions
core
StandardLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
sq
stable
equal
A
:Type,
x
,
y
:
A
. SqStable(
x
=
y
)
By:
Unfold `sq_stable` 0 THEN UnivCD
Generated subgoal:
1
1.
A
: Type
2.
x
:
A
3.
y
:
A
4.
(
x
=
y
)
x
=
y
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(2steps total)
PrintForm
Definitions
core
StandardLIB
Doc
A:Type, x,y:A. SqStable(x = y) A:Type, x,y:A. SqStable(x = y)
(x = y)
x = y
