Nuprl - Proof: hhd wd 1

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

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

mt(cons(h; t))

By:	Simp THEN Try (Complete Auto) THEN Simpsetp [`nlogic`]

Generated subgoals:

None

About:

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