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

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

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

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

n = 0

cons(h; t)[n] = 1of(rep_list('a;t))(pre(n))

By:	Assert (n>0) THEN HN THEN Simp

Generated subgoals:

1 7. n>0
n<||cons(h; t)||
1 step

2 7. n>0
cons(h; t)[n] = 1of(rep_list('a;t))(n-1) 'a
2 steps

About:

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

1	7. n>0 n<\|\|cons(h; t)\|\|	1 step
2	7. n>0 cons(h; t)[n] = 1of(rep_list('a;t))(n-1) 'a	2 steps