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