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

By:

Unfold `ma-compatible` 0 THEN All_MsgA THEN Analyze 0 THEN Unfold_MsgA -1 THEN RW (AddrC [2] (UnfoldTopC `and` THENC FoldTopC `cand`)) 0 THEN Try 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 (Unfold `ma-valtype` 0) THEN Try (BackThru (Thm* eq:EqDecider(X), f,g:x:X fp-> Type, x:X. g  f  (f(x)?T r g(x)?Top)) 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* B1,B2:(AType), eq:EqDecider(A), f:a:A fp-> B1(a), g:a:A fp-> B2(a). (Thm* f  f  g) THEN Try (BackThru (Thm* B:(AType), eq:EqDecider(A), f,g:a:A fp-> B(a). f || g  g  f  g) THEN Try (BackThru `subtype-fpf-cap5`)

None

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