bool
1
Sections
StandardLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Theorem
Name
Thm*
i
,
j
:
. (
i
=
j
) = false
i
j
[eq_int_eq_false_elim]
cites the following:
Thm*
i
,
j
:
.
i
=
j
(
i
=
j
) = true
[eq_int_eq_true]
Thm*
true
= false
[btrue_neq_bfalse]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
bool
1
Sections
StandardLIB
Doc
i,j:
. (i=
j) = false 
i 
ji,j:. i = j (i=j) = true
true = falsei,j:. (i=j) = false i ji,j:. i = j (i=j) = truetrue = false