1. x : Id
2. tg : Id
3. k : Knd
4. l : IdLnk
5. T : Type
6. A : Type
7. B : Type
8. AB(T List)
9. rcv(l; tg) = k  T = B
10. x : A  x:Id fp-> Type
11. k : B  rcv(l; tg) : T  k:Knd fp-> Type
12. State(x : A)
13. ma-valtype(k : B  rcv(l; tg) : T; k)
  ma-valtype(k : B  rcv(l; tg) : T; k) r B

By:	Unfold `ma-valtype` 0 THEN RWO Thm* eq:EqDecider(A), f,g:a:A fp-> Top, x:A, z:Top. Thm* f  g(x)?z ~ if x  dom(f) f(x)?z else g(x)?z fi 0 THEN Reduce 0 THEN SplitOnConclITE THEN Analyze -1 THEN RWO Thm* eq:EqDecider(A), x,y:A, v:Top. x  dom(y : v)  x = y 0

None

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