IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hisr wd 'a,'b:S. and(all(x:'b. isr(inr(x))),all(y:'a. not(isr(inl(y)))))
By:
Unab [`hisr`] THEN HN THEN StrongAuto 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
'a,'b:S. and(all(
x:'b. isr(inr(x))),all(
