(37steps total) PrintForm Definitions Lemmas hol list 1 Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: list iso 2 2 1 1 1

1. 'a : S
2. x : ('a)
3. f : 'a
4. n : 
5. x = <m:. if m<n then f(m) else @x:'a. true fi ,n>
  x':'a List. 
  <m:. if m<n then f(m) else @x:'a. true fi ,n> = rep_list('a;x')


By: DTerm (f{n}) 0 THEN Simp THEN StrongAuto


Generated subgoals:

1   f  n'a
3 steps
2   <m:. if m<n then f(m) else @x:'a. true fi ,n> = rep_list('a;f{n})
10 steps

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

(37steps total) PrintForm Definitions Lemmas hol list 1 Sections HOLlib Doc