(2steps total) PrintForm Definitions Lemmas mb event system 6 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: d-sub transitivity
  D1,D2,D3:Dsys. D1  D2  D2  D3  D1  D3
By: Auto THEN All (Unfold `d-sub`) THEN ExRepD THEN BetterSplitAndConcl

Generated subgoal:

1 1. D1 : Dsys
2. D2 : Dsys
3. D3 : Dsys
4. i:Id. M(i)  M(i)
5. i:Id. M(i)  M(i)
6. i : Id
  M(i)  M(i)
1 step

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

(2steps total) PrintForm Definitions Lemmas mb event system 6 Sections EventSystems Doc