es:ES, i,x:Id, T:Type, I:(TProp).
  (vartype(i;x) r T) & e@i.first(e)  I((x when e))
  
  e@i.I((x when e))  I((x after e))  @i always.I(x)

By:

let tac let  AllHyps SetHD THEN Try DoSubsume let  THEN let  AllHyps (h.NthHypEq h THEN RepeatFor 2 Analyze THEN EsAuto) in UnivCD THEN ExRepD THEN Try (Complete tac) THEN Unfold `alle-at1` 0 THEN BackThru Thm* es:ES, i:Id, P:({e:E| loc(e) = i  Id }Prop). Thm* e@i.P(e)  e@i.first(e)  P(e) & e@i.first(e)  P(pred(e))  P(e) THEN Try (Complete tac) THEN All (Unfold `alle-at`) THEN Try (Complete tac) THEN InstHyp [pred(e)] -5 THEN EsAuto THEN Subst ((x after pred(e)) = (x when e)) -1 THEN EsAuto THEN tac

None

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