(17steps total)
PrintForm
Definitions
Lemmas
mb
list
2
Sections
MarkB
generic
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
flip
lemma
1
1
1.
k
:
2.
x
:
k
3.
y
:
k
4.
z
:
k
5.
y
=
z
6.
x
=
y
7.
x1
:
k
8.
x1
=
x
(
z
=
z
) = true
By:
BackThru
Thm*
i
,
j
:
.
i
=
j
(
i
=
j
) = true
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(17steps total)
PrintForm
Definitions
Lemmas
mb
list
2
Sections
MarkB
generic
Doc
y = z
(z=
z) = true
i,j:
. i = j 
(i=
