(9steps total) PrintForm Definitions mb event system 1 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: fun exp add sq
  n,m:, f,i:Top. (f^n+m(i)) ~ (f^n(f^m(i)))
By: InductionOnNat

Generated subgoals:

1   m:, f,i:Top. (f^0+m(i)) ~ (f^0(f^m(i)))
1 step
2 1. n : 
2. 0<n
3. m:, f,i:Top. (f^n-1+m(i)) ~ (f^n-1(f^m(i)))
  m:, f,i:Top. (f^n+m(i)) ~ (f^n(f^m(i)))
7 steps

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

(9steps total) PrintForm Definitions mb event system 1 Sections EventSystems Doc