IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hcons def12111 1. 'a : S
2. h : 'a 3. t : hlist('a)
4. n : if n<||t||+1 then cons(h; t)[n] else arb('a) fi
=
if n = 0 then h else 1of(rep_list('a;t))(pre(n)) fi
By:
BifCase THEN Simp THEN StrongAuto THEN BifCase THEN Simp THEN StrongAuto