∀a,tg,l:Top.  (rcv(l,tg) = locl(a) ~ ff)
{ (UnivCD THENA Auto) }
1. a : Top@i
2. tg : Top@i
3. l : Top@i
⊢ rcv(l,tg) = locl(a) ~ ff