(16steps 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-set
  A,B:Type.
  strong-subtype(A;B)
  
  (P:(AProp), Q:(BProp).
  ((x:A. P(x)  Q(x))  strong-subtype({x:A| P(x) };{x:B| Q(x) }))
By: Unfold `strong-subtype` 0 THEN ExRepD

Generated subgoals:

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

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

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