---

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


1. tg : Id@i
2. links : IdLnk List@i
3. y : Id@i
4. ↑isrcv(inr y )@i
5. tag(inr y ) = tg ∈ Id@i
6. (lnk(inr y ) ∈ links)@i
7. (lnk(inr y ) ∈ links)
⊢ (inr y ) = rcv(lnk(inr y ),tag(inr y )) ∈ Knd
BY
{ (All (RepUR ``isrcv``) THEN Auto) }

---

Latex:



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


By

(All  (RepUR  ``isrcv``)  THEN  Auto)

---

Home Index