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

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

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

n<||t||+1
6.

n = 0

arb('a) = 1of(rep_list('a;t))(pre(n))

By:	Unab [`rep_list`] THEN Simp THEN StrongAuto THEN BifCase THEN HN THEN Simp

Generated subgoals:

None

About:

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