IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
ma-ef wf M:MsgA, k:Knd, s:M.state, v:M.da(k), x:Id, w:M.ds(x). M.ef(k,x,s,v,w) Prop
By:
All_MsgA THEN Unfold `fpf-val` 0 THEN DoSubsume THEN Reduce 0
THEN
All (Unfold `ma-valtype`)
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
M:MsgA, k:Knd, s:M.state, v:M.da(k), x:Id, w:M.ds(x). M.ef(k,x,s,v,w) 
Prop
