(17steps total) PrintForm Definitions Lemmas mb event system 5 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: ma-single-effect1 wf
  x,y:Id, k:Knd, A,B,T:Type, f:(ABTA).
  y = x  ma-single-effect1(x;A;y;B;k;T;f)  MsgA
By: Auto THEN Unfold `ma-single-effect1` 0 THEN Analyze THEN Try (Complete Auto)

Generated subgoal:

1 1. x : Id
2. y : Id
3. k : Knd
4. A : Type
5. B : Type
6. T : Type
7. f : ABTA
8. y = x
  (s,v. f(s(x),s(y),v))
   State(x : A  y : B)ma-valtype(k : T; k)x : A  y : B(x)?Void
16 steps

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

(17steps total) PrintForm Definitions Lemmas mb event system 5 Sections EventSystems Doc