Nuprl - Proof: hcons def 1 2 1 1 1 2 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hcons def 1 2 1 1 1 2 1

1. 'a : S
2. h : 'a
3. t : hlist('a)
4. n :

5. n<||t||+1
6.

n = 0
7. n>0

n<||cons(h; t)||

By:	Simpsetp [`hol_to_nuprl`;`nat_to_int`] THEN StrongAuto THEN Try (Complete (Unfold `label` 0))

Generated subgoals:

None

About:

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