---

Step * 1 1 1 1 of Lemma member-rcvs-on


1. tg : Id@i
2. links : IdLnk List@i
3. k : Knd@i
4. ↑isrcv(k)@i
5. tag(k) = tg ∈ Id@i
6. (lnk(k) ∈ links)@i
7. (lnk(k) ∈ links)
⊢ k = rcv(lnk(k),tg) ∈ Knd
BY
{ RevHypSubst'(-3) 0 }

1
1. tg : Id@i
2. links : IdLnk List@i
3. k : Knd@i
4. ↑isrcv(k)@i
5. tag(k) = tg ∈ Id@i
6. (lnk(k) ∈ links)@i
7. (lnk(k) ∈ links)
⊢ k = rcv(lnk(k),tag(k)) ∈ Knd

---

Latex:



1.  tg  :  Id@i
2.  links  :  IdLnk  List@i
3.  k  :  Knd@i
4.  \muparrow{}isrcv(k)@i
5.  tag(k)  =  tg@i
6.  (lnk(k)  \mmember{}  links)@i
7.  (lnk(k)  \mmember{}  links)
\mvdash{}  k  =  rcv(lnk(k),tg)


By

RevHypSubst'(-3)  0

---

Home Index