Nuprl - Proof: cons char 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: cons char 1

'a:S, l:hlist('a).

mt(l)

cons((hd(l)); tl(l)) = l

'a:S, l:'a List.

mt(l)

cons(head(l); tl(l)) = l

By:

Generated subgoals:

None

About:

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