Nuprl - Proof: head wf 1

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

1. 'a : Type
2. l : 'a List
3.

mt(l)

head(l)

By:	ListInd 2 THEN StrongAuto THEN Try (Complete (Unfold `label` 0)) THEN Unab [`head`;`hd`;`mt`] THEN All AbReduce THEN StrongAuto THEN Try (Complete (Unfold `label` 0))

Generated subgoal:

1 3. True
"?" 'a
1 step

About:

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