(19steps total) PrintForm Definitions Lemmas 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: finite-set-type
  T:Type, P:(TProp).
  (x:T. SqStable(P(x)))
  
  (finite-type({x:T| P(x) })  (L:T List. x:T. P(x)  (x  L)))
By: RepeatFor 3 (Analyze 0)
THEN
RWO Thm* finite-type(T)  (L:T List. x:T. (x  L)) 0
THEN
ExRepD
THEN
InstConcl [L]

Generated subgoals:

1 1. T : Type
2. P : TProp
3. x:T. SqStable(P(x))
4. L : {x:T| P(x) } List
5. x:{x:T| P(x) }. (x  L)
6. x : T
7. P(x)
  (x  L)
1 step
2 1. T : Type
2. P : TProp
3. x:T. SqStable(P(x))
4. L : {x:T| P(x) } List
5. x:{x:T| P(x) }. (x  L)
6. x : T
7. (x  L)
  P(x)
2 steps
3 1. T : Type
2. P : TProp
3. x:T. SqStable(P(x))
4. L : T List
5. x:T. P(x)  (x  L)
  L  {x:T| P(x) } List
5 steps
4 1. T : Type
2. P : TProp
3. x:T. SqStable(P(x))
4. L : T List
5. x:T. P(x)  (x  L)
6. x : {x:T| P(x) }
  (x  L)
10 steps

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

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