Nuprl - Proof: flatten wf

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

'a:Type, l:('a List) List. flatten(l)

'a List

By:	Id THEN StrongAuto THEN Try (Complete (Unfold `label` 0)) THEN ((ListInd 2) THEN (RecUnfold `flatten` 0)) THEN Simp THEN StrongAuto

Generated subgoals:

None

About:

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