M1,M2:MsgA. M1  M2  Prop{i'}

By:

Auto THEN Unfold_MsgA -2 THEN Unfold_MsgA -1 THEN DoSubsume THEN Try (BackThru (Thm* B1,B2:(AType). (Thm* (a:A. B1(a) r B2(a))  (a:A fp-> B1(a) r a:A fp-> B2(a))) THEN Repeat UseSubtypeRelLemmas THEN Try (BackThru (Thm* eq:EqDecider(X), f,g:x:X fp-> Type, x:X. f  g  (f(x)?Void r g(x)?T)) THEN Try (BackThru (Thm* eq:EqDecider(X), f,g:x:X fp-> Type, x:X. g  f  (f(x)?T r g(x)?Top))

None

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