(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
2
2
2
1
1.
k
:
2.
x
:
k
3.
y
:
k
4.
z
:
k
5.
y
=
z
6.
x
=
y
7.
x1
:
k
8.
x1
=
x
9.
x1
=
y
10.
x1
=
z
(
x1
=
z
) = false
By:
BackThru
Thm*
i
,
j
:
.
i
j
(
i
=
j
) = false
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
(x1=
z) = false
i,j:
. i 
j 
(i=
