IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
s-sends-rule1121 1. x : Id
2. tg : Id
3. k : Knd
4. l : IdLnk
5. T : Type
6. A : Type
7. B : Type
8. f : AB(T List)
9. rcv(l; tg) = kT = B 10. x : Ax:Id fp-> Type
11. k : B rcv(l; tg) : Tk:Knd fp-> Type
12. s : State(x : A)
13. v : ma-valtype(k : B rcv(l; tg) : T; k)
14. f(s(x),v) = f(s(x),v)
15. T List
16. T List
17. T 18. rcv(l; tg) = k 19. k : Bk:Knd fp-> Type
Tr B
By:
SubtypeRelEq THEN BackThruSomeHyp
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html