∀tg,l:Top.  (tag(rcv(l,tg)) ~ tg)
{ (UnivCD THENA Auto) }
1. tg : Top@i
2. l : Top@i
⊢ tag(rcv(l,tg)) ~ tg