Def i=j == if i=j true ; false fi

is mentioned by

Thm* x,y:A, P:(AProp), i,j:. Thm* P(if i=j x else y fi)  P(if i=j x else y fi)	[eq_int_cases_test]
Thm* i,j:. (i=j) = true  i = j	[eq_int_eq_true_elim]
Thm* i,j:. (i=j) = false  i  j	[eq_int_eq_false_elim]
Thm* i,j:. i = j  (i=j) = true	[eq_int_eq_true]
Thm* i,j:. i  j  (i=j) = false	[eq_int_eq_false]
Thm* x,y:. x=y  x = y	[assert_of_eq_int_rw]
Thm* x,y:. x=y  x  y	[neg_assert_of_eq_int]
Thm* x,y:. x=y  x = y	[assert_of_eq_int]

Try larger context: StandardLIB IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html