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

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

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:	Simpsetp [`nat_to_int`]

Generated subgoal:

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

About:

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