(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 3
1. 'a : S
2. h : 'a
3. t : hlist('a)
4. n : 
5. n<||t||+1
6. n = 0
  arb('a) = h
By: Simpsetp [`nat_to_int`] THEN StrongAuto

Generated subgoal:

1   arb('a) = h
1 step

About:
natural_numberaddless_thanequal
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