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