---

Step * 1 1 of Lemma rcv_one_one


1. l1 : IdLnk
2. l2 : IdLnk
3. tg1 : Id
4. tg2 : Id
5. (inl <l1, tg1>) = (inl <l2, tg2>) ∈ (IdLnk × Id + Id)
⊢ (l1 = l2 ∈ IdLnk) ∧ (tg1 = tg2 ∈ Id)
BY
{ Obvious }

---

Latex:



1.  l1  :  IdLnk
2.  l2  :  IdLnk
3.  tg1  :  Id
4.  tg2  :  Id
5.  (inl  <l1,  tg1>)  =  (inl  <l2,  tg2>)
\mvdash{}  (l1  =  l2)  \mwedge{}  (tg1  =  tg2)


By

Obvious

---

Home Index