Nuprl - Proof: ma-single-pre1 wf 1

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

1. Id
2. T : Type
3. A : Type
4. x : Id
5. A

Prop
6. s : State(x : A)

s(x)

By:	Repeat (Unfolds [`ma-state`;`fpf-cap`;`fpf-single`;`fpf-dom`;`fpf-ap`] -1 (THEN (Reduce -1) THEN DoSubsume

Generated subgoal:

1 6. x@0:Idif eqof(IdDeq)(x,x@0) false A else Top fi
if eqof(IdDeq)(x,x) false A else Top fi r A
1 step

About:

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