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
) = true
i
=
j
[eq_int_eq_true_elim]
cites the following:
Thm*
i
,
j
:
.
i
j
(
i
=
j
) = false
[eq_int_eq_false]
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) = true 
i = ji,j:. i 
j (i=j) = false
true = falsei,j:. (i=j) = true i = ji,j:. i j (i=j) = falsetrue = false