IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
recognizer1 feasible T,A:Type, P:(AT), k:Knd, i,r,x:Id.
ATx = r d-feasible(loc.(recognizer1(loc;T;A;P;k;i;r;x)))
By:
ProveFeasibleSupport [i]
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
T,A:Type, P:(A
T
), k:Knd, i,r,x:Id.
A 
T 
x = r 
loc.
(recognizer1(loc;T;A;P;k;i;r;x)))
