IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
ma-single-frame wf x:Id, L:Knd List, t:Type. only members of L affect x :t MsgA
By:
Auto THEN Unfold `ma-single-frame` 0 THEN Analyze THEN Reduce 0
THEN
Assert (x : tx:Id fp-> Type)
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
x:Id, L:Knd List, t:Type. only members of L affect x :t 
MsgA
