Nuprl - Proof: ma-single-frame-ma-single-frame-compatible

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

x:Id, L:Top, t:Type, x1:Id, L1:Top, t1:Type.

x = x1

only members of L affect x :t ||+ only members of L1 affect x1 :t1

By:	ProveBaseCompatTac

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