(13steps total) PrintForm Definitions mb event system 1 Sections EventSystems Search Doc
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: strong-subtype transitivity
  A,B,C:Type.
  strong-subtype(A;B)  strong-subtype(B;C)  strong-subtype(A;C)
By: Auto THEN All (Unfold `strong-subtype`) THEN ExRepD THEN Analyze 0

Generated subgoals:

1 1. A : Type
2. B : Type
3. C : Type
4. A r B
5. {b:B| a:A. b = a  B } r A
6. a1,a2:A. a1 = a2  B  a1 = a2
7. B r C
8. {b:C| a:B. b = a  C } r B
9. a1,a2:B. a1 = a2  C  a1 = a2
  A r C
1 step
2 1. A : Type
2. B : Type
3. C : Type
4. A r B
5. {b:B| a:A. b = a  B } r A
6. a1,a2:A. a1 = a2  B  a1 = a2
7. B r C
8. {b:C| a:B. b = a  C } r B
9. a1,a2:B. a1 = a2  C  a1 = a2
10. A r C
  ({b:C| a:A. b = a  C } r A) & (a1,a2:A. a1 = a2  C  a1 = a2)
11 steps

About:
setuniverseequalsubtype_relimpliesallexists
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

(13steps total) PrintForm Definitions mb event system 1 Sections EventSystems Search Doc