(7steps total) PrintForm Definitions sqequal 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: eq int eq true elim sqequal 1 1
1. i : 
2. j : 
3. (i=j) ~ true
  i = j
By: p.
let x,y  dest_sqequal (h -1 p) in
(Assert (mk_equal_term bool_term y y)
(THENL
([Auto;SqSubstAtAddr [2] x -1 THENL [Trivial;Id]])
p

Generated subgoal:

1 4. (i=j) = true
  i = j
1 step

About:
btrueintequalsqequal
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(7steps total) PrintForm Definitions sqequal 1 Sections StandardLIB Doc