Nuprl - Proof: ma-single-pre-init wf

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

a:Id, T:Type, ds:x:Id fp-> Type, P:(State(ds)

Prop),

init:x:Id fp-> ds(x)?Void.

(with ds: ds init: initaction a:T precondition a(v) is P)

MsgA

By:	Unfold `ma-single-pre-init` 0 THEN ReduceFpf 0 THEN Unfold `ma-valtype` 0 THEN Reduce 0

Generated subgoals:

None

About:

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