Nuprl - Proof: ma-single-pre wf 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. a : Id
2. T : Type
3. ds : x:Id fp-> Type
4. State(ds)

Prop
5. x : Id
6. x = a

False
7. State(ds)
8. true

eqof(KindDeq)(locl(a),locl(x))

By:	RWO "deq_property<" 0 THEN SplitOrHyps

Generated subgoal:

1 6. x = a
7. State(ds)
8. true
locl(a) = locl(x)
1 step

About:

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