Nuprl - Proof: ma-state-subtype 1

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 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

By:	MoveToConcl -1 THEN Try (BackThru (Thm* eq:EqDecider(X), f,g:x:X fp-> Type. (Thm* g f (x:X. f(x)?Top r g(x)?Top))

Generated subgoals:

None

About:

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