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

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

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

Prop
5. x : Id
6. x = a
7. State(ds)
8. true

locl(a) = locl(x)

By:

Analyze

Generated subgoals:

None

About:

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