the_w:World, l:IdLnk, t,t':.
  match(l;t;t')
  
  ||snds(l;t)||||rcvs(l;t')||
  & ||rcvs(l;t')||<||snds(l;t)||+||onlnk(l;m(source(l);t))||

By:	UnivCD THEN Unfold `w-match` 0 THEN Assert (||onlnk(l;m(source(l);t))||  )

1	1. the_w : World 2. l : IdLnk 3. t :  4.    ||onlnk(l;m(source(l);t))||	1 step
2	1. the_w : World 2. l : IdLnk 3. t :  4. t' :  5. ||onlnk(l;m(source(l);t))||     ((||snds(l;t)||||rcvs(l;t')||)   ((||rcvs(l;t')||<||snds(l;t)||+||onlnk(l;m(source(l);t))||))      ||snds(l;t)||||rcvs(l;t')||   & ||rcvs(l;t')||<||snds(l;t)||+||onlnk(l;m(source(l);t))||	1 step

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