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