Nuprl - Proof: ma-state-subtype

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: ma-state-subtype

ds,ds':ltg:Id fp-> Type. ds

ds'

(State(ds')

r State(ds))

By:	Auto THEN Unfold `ma-state` 0 THEN Reduce 0 THEN UseSubtypeRelLemmas

Generated subgoal:

1 1. ds : ltg:Id fp-> Type
2. ds' : ltg:Id fp-> Type
3. ds ds'
4. x : Id
ds'(x)?Top r ds(x)?Top
1 step

About:

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html