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

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

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

n<||t||+1
6. n = 0

arb('a) = h

By:	Inst Thm* l:A List. \|\|l\|\|0 ['a;t] 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