IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
eqmod fun1 1. m :
2. a :
3. a' :
4. b :
5. b' :
6. a = a' mod m 7. b = b' mod m 8. a = b mod m a' = b' mod m
By:
(FwdThru Thm*m,a,b:. (a = b mod m) (b = a mod m) [6]) THEN (Thin 6)