(17steps total) PrintForm Definitions Lemmas mb event system 6 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: frame-rule 1
1. i : Id
2. L : Knd List
3. x : Id
4. T : Type
  (es.(vartype(i;x) r T)
  (& (e:E. 
  (& (loc(e) = i  Id
  (& (
  (& (((x after e) = (x when e)  T  (kind(e)  L))
  (& (& ((kind(e)  L)  (x after e) = (x when e)  T)))
   {es:ES| es is an event system of @i: only L affects x : T }Prop{i'}
By: Analyze THEN Analyze -1 THEN Analyze -1 THEN ExRepD THEN Try DoSubsume
THEN
Try (HypSubst -1 0)
THEN
Try (HypSubst -2 0)

Generated subgoals:

None

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

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