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

1. 'a : S
2. h : 'a
3. t : hlist('a)
4. n : 
  if n<||t||+1 then cons(ht)[n] else arb('a) fi 
  =
  if n = 0 then h else 1of(rep_list('a;t))(pre(n)) fi 


By: BifCase THEN Simp THEN StrongAuto THEN BifCase THEN Simp THEN StrongAuto


Generated subgoals:

1 5. n<||t||+1
6. n = 0  
  cons(ht)[n] = h  'a

1 step
2 5. n<||t||+1
6. n = 0  
  cons(ht)[n] = 1of(rep_list('a;t))(pre(n))  'a

4 steps
3 5. n<||t||+1
6. n = 0  
  arb('a) = h

2 steps
4 5. n<||t||+1
6. n = 0  
  arb('a) = 1of(rep_list('a;t))(pre(n))

2 steps

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

(17steps total) PrintForm Definitions Lemmas hol list 2 Sections HOLlib Doc