Nuprl - Proof: ma-single-effect wf

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: ma-single-effect wf

x:Id, k:Knd, ds:x:Id fp-> Type, da:a:Knd fp-> Type,

f:(State(ds)

ma-valtype(da; k)

ds(x)?Void).

ma-single-effect(ds; da; k; x; f)

MsgA

By:	Auto THEN Unfold `ma-single-effect` 0 THEN Analyze THEN Reduce 0

Generated subgoals:

None

About:

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