the_w:World, l:IdLnk, mss:Msg List.
Thm* withlnk(l;mss)
(t:Id
the_w.M(l,t)) Lista,b:IdLnk. a = b 
a = b| Theorem | Name |
| the_w:World, l:IdLnk, mss:Msg List.
Thm* withlnk(l;mss) (t:Idthe_w.M(l,t)) List | [w-withlnk_wf] |
| cites the following: | |
| a,b:IdLnk. a = b a = b | [assert-eq-lnk] |