the_w:World, l:IdLnk, i:Id, a:Action(i).
Thm* isrcv(l;a)
isnull(a) & isrcv(kind(a)) & lnk(kind(a)) = la,b:IdLnk. a = b 
a = b| Theorem | Name |
| the_w:World, l:IdLnk, i:Id, a:Action(i).
Thm* isrcv(l;a) isnull(a) & isrcv(kind(a)) & lnk(kind(a)) = l | [assert-w-isrcvl] |
| cites the following: | |
| a,b:IdLnk. a = b a = b | [assert-eq-lnk] |