1. i : Id
2. L : Knd List
3. x : Id
4. T : Type
5. w : World
6. FairFifo
7. FairFifo
8. vartype(i;x) r T
9. e1 : Id
10. e2 : 
11. isnull(a(e1;e2))  [not for witness]
12. e1 = i
13. isnull(a(i;e2))
14. islocal(kind(a(i;e2)))
14. 
14. deq-member(IdDeq;act(kind(a(i;e2)));1of())
14. 
14. 2of()(act(kind(a(i;e2))),x.s(i;e2).x,val(a(i;e2)))
15. (True  (kind(a(i;e2))  L))  s(i;e2).x = s(i;e2+1).x
  Dec((kind(a(e1;e2))  L))

By:	AssertBY Dec(deq-member(KindDeq;kind(a(e1;e2));L)) Auto THEN RWO Thm* eq:EqDecider(A), L:A List, x:A. deq-member(eq;x;L)  (x  L) -1

None

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