Nuprl - Proof: hisl wd

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hisl wd

'b,'a:S. and(all(

x:'a. isl(inl(x))),all(

y:'b. not(isl(inr(y)))))

By:	Unab [`hisl`] THEN HN THEN Try (Complete Auto) THEN Try (Complete (Unfold `label` 0))

Generated subgoals:

None

About:

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html