IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
kindcase wf B:Type, k:Knd, f:(IdB), g:(IdLnkIdB).
kindcase(k;a.f(a);l,t.g(l,t)) B
By:
Auto THEN KindCase 2
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html