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