---

Step * of Lemma rcv_rcv_lemma

∀t',l',t,l:Top.  (rcv(l,t) = rcv(l',t') ~ l = l' ∧b t = t')
BY
{ (UnivCD THENA Auto) }

1
1. t' : Top@i
2. l' : Top@i
3. t : Top@i
4. l : Top@i
⊢ rcv(l,t) = rcv(l',t') ~ l = l' ∧b t = t'

---

Latex:


\mforall{}t',l',t,l:Top.    (rcv(l,t)  =  rcv(l',t')  \msim{}  l  =  l'  \mwedge{}\msubb{}  t  =  t')


By

(UnivCD  THENA  Auto)

---

Home Index