Nuprl - Proof: possible-world-monotonic 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: possible-world-monotonic 1

1. A : Dsys
2. B : Dsys
3. A

B
4. w : World
5.

i,x:Id. vartype(i;x)

r M(i).ds(x)

i,x:Id. vartype(i;x)

r M(i).ds(x)

By:	Auto THEN Using [`B',M(i).ds(x)] (BackThru Thm* (A r B) (B r C) (A r C)) THEN Try BackThruSomeHyp THEN BackThru Thm* M1,M2:MsgA, x:Id. M1 M2 (M2.ds(x) r M1.ds(x)) THEN AllHyps (h.Unfold `d-sub` h THEN BackThru h)

Generated subgoals:

None

About:

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