(70steps total) PrintForm Definitions Lemmas mb event system 7 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: s-sends-rule1 1 2 1

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(ltg) = k  T = B
10. x : A  x:Id fp-> Type
11. k : B  rcv(ltg) : T  k:Knd fp-> Type
12. s : State(x : A)
13. v : ma-valtype(k : B  rcv(ltg) : Tk)
14. f(s(x),v) = f(s(x),v)
15. T List
16. T List
17. T
18. rcv(ltg) = k
19. k : B  k:Knd fp-> Type
  T B


By: SubtypeRelEq THEN BackThruSomeHyp


Generated subgoals:

None

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

(70steps total) PrintForm Definitions Lemmas mb event system 7 Sections EventSystems Doc