ltg:(IdLnkIdType), i:Id, k:Knd, T:Type.
  (ltg  da-outlinks(k : T;i))
  
  isrcv(k) & source(lnk(k)) = i
  & (1of(ltg) ~ lnk(k))
  & (1of(2of(ltg)) ~ tag(k))
  & 2of(2of(ltg)) = T

By:

Unfold `guard` 0 THEN RepeatFor 5 (Analyze 0 THENA Complete Auto) THEN Repeat (Unfolds ([`fpf-dom-list` (;`da-outlink-f` (;`has-src` (;`isrcv` (;`lnk` (;`tagof` (;`da-outlinks` (;`fpf-single` (;`mapfilter`] (-1 (THEN (Reduce -1) THEN AssertBY ((ltg  nil)) (RWO Thm* x:T. (x  nil)  False 0) THEN DVar `k' THEN Unfold `fpf-ap` -2 THEN Reduce -2 THEN Unfolds [`isrcv`;`lnk`;`tagof`] 0 THEN Reduce 0 THEN Try (SplitOnHypITE -2 THEN Reduce -3) THEN Try (Complete Auto) THEN RWO Thm* a,x:T. (x  [a])  x = a -3 THEN HypSubst -3 0 THEN Reduce 0

None

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