---

Step * of Lemma rcv_one_one

∀[l1,l2:IdLnk]. ∀[tg1,tg2:Id].  {(l1 = l2 ∈ IdLnk) ∧ (tg1 = tg2 ∈ Id)} supposing rcv(l1,tg1) = rcv(l2,tg2) ∈ Knd
BY
{ Auto }

1
1. l1 : IdLnk
2. l2 : IdLnk
3. tg1 : Id
4. tg2 : Id
5. rcv(l1,tg1) = rcv(l2,tg2) ∈ Knd
⊢ {(l1 = l2 ∈ IdLnk) ∧ (tg1 = tg2 ∈ Id)}

---

Latex:


\mforall{}[l1,l2:IdLnk].  \mforall{}[tg1,tg2:Id].    \{(l1  =  l2)  \mwedge{}  (tg1  =  tg2)\}  supposing  rcv(l1,tg1)  =  rcv(l2,tg2)


By

Auto

---

Home Index