Nuprl - Proof: strong-subtype-set2

(5steps 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-set2

A:Type, P:(A

Prop). strong-subtype({x:A| P(x) };A)

By:	Unfold `strong-subtype` 0

Generated subgoals:

1 1. A : Type
2. P : AProp
  {x:A| P(x) } r A
1 step

2 1. A : Type
2. P : AProp
  {b:A| a:{x:A| P(x) }. b = a } r {x:A| P(x) }
2 steps

3 1. A : Type
2. P : AProp
3. a1 : {x:A| P(x) }
4. a2 : {x:A| P(x) }
5. a1 = a2
  a1 = a2
1 step

About:

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

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

1	1. A : Type 2. P : AProp {x:A\| P(x) } r A	1 step
2	1. A : Type 2. P : AProp {b:A\| a:{x:A\| P(x) }. b = a } r {x:A\| P(x) }	2 steps
3	1. A : Type 2. P : AProp 3. a1 : {x:A\| P(x) } 4. a2 : {x:A\| P(x) } 5. a1 = a2 a1 = a2	1 step