(9steps total) PrintForm Definitions Lemmas mb event system 1 Sections EventSystems Search Doc
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: filter map upto2
  t',m:, T:Type, f:(T), P:(T).
  m+1||filter(P;map(f;upto(t')))||
  
  (t:. P(f(t)) & ||filter(P;map(f;upto(t)))|| = m  )
By: InductionOnNat

Generated subgoals:

1   m:, T:Type, f:(T), P:(T).
  m+1||filter(P;map(f;upto(0)))||
  
  (t:. P(f(t)) & ||filter(P;map(f;upto(t)))|| = m  )
1 step
2 1. t' : 
2. 0<t'
3. m:, T:Type, f:(T), P:(T).
3. m+1||filter(P;map(f;upto(t'-1)))||
3. 
3. (t:. P(f(t)) & ||filter(P;map(f;upto(t)))|| = m  )
  m:, T:Type, f:(T), P:(T).
  m+1||filter(P;map(f;upto(t')))||
  
  (t:. P(f(t)) & ||filter(P;map(f;upto(t)))|| = m  )
7 steps

About:
boolassertintnatural_numberaddapplyfunctionuniverse
equalimpliesandallexists
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

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