Nuprl - Proof: ma-single-pre wf 1

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

1. a : Id
2. T : Type
3. ds : x:Id fp-> Type
4. P : State(ds)

Prop

a : P

a@0:Id fp-> State(ds)

ma-valtype(locl(a) : T; locl(a@0))

Prop

By:	Repeat (Unfolds [`ma-valtype`;`fpf`;`fpf-single`;`fpf-dom`;`fpf-cap`;`fpf-ap`] 0 (THEN (Reduce 0) THEN RepeatFor 3 (Analyze THEN Try (Complete Auto))

Generated subgoal:

1 5. x : {a@0:Id| (a@0 [a]) }
6. State(ds)
if eqof(KindDeq)(locl(a),locl(x)) false T else Top fi T
4 steps

About:

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