Nuprl - Proof: list 2 decomp

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: list 2 decomp

T:Type, z:T List. ||z|| = 2

z = [z[0]; z[1]]

By:	((Analyze 0) THEN (Analyze 0)) THEN ListInd -1 THEN Reduce 0 THEN Try (Complete Auto) THEN ListInd -2 THEN Reduce 0 THEN Try (Complete Auto) THEN ListInd -2 THEN Reduce 0 THEN Try (Complete Auto)

Generated subgoals:

None

About:

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