1. M:MsgAForm. ma-is-empty(M)  
  L:MsgA List. ma-is-empty((L))  

By:	Inst Thm* L:MsgA List. (L)  MsgAForm []

1

2. L:MsgA List. (L)  MsgAForm   L:MsgA List. ma-is-empty((L))

1 step

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html