1. A : Dsys
2. B : Dsys
3. A  B
4. w : World
5. i,x:Id. vartype(i;x) r M(i).ds(x)
6. i:Id, a:Action(i). isnull(a)  (valtype(i;a) r M(i).da(kind(a)))
7. l:IdLnk, tg:Id. (w.M(l,tg)) r M(source(l)).da(rcv(l; tg))
8. i,x:Id. M(i).init(x,s(i;0).x)
  i,x:Id. M(i).init(x,s(i;0).x)

By:	Auto THEN Using [`M2',M(i);`V',(x. M(i).ds(x))] (BackThru (Thm* V:(IdType), M1,M2:MsgA. (Thm* (x:Id. V(x) r M2.ds(x)) (Thm*  (Thm* M1  M2  (x:Id, v:V(x). M2.init(x,v)  M1.init(x,v))) THEN Try BackThruSomeHyp THEN AllHyps (h.Unfold `d-sub` h THEN BackThru h) THEN DoSubsume THEN BackThruSomeHyp

None

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