---

Step * of Lemma not_rcv_locl

∀[a:Id]. ∀[l:IdLnk]. ∀[tg:Id].  False supposing rcv(l,tg) = locl(a) ∈ Knd
BY
{ (Unfolds ``Knd locl`` 0 THEN Auto) }

1
1. a : Id
2. l : IdLnk
3. tg : Id
4. rcv(l,tg) = (inr a ) ∈ (IdLnk × Id + Id)
⊢ False

---

Latex:


\mforall{}[a:Id].  \mforall{}[l:IdLnk].  \mforall{}[tg:Id].    False  supposing  rcv(l,tg)  =  locl(a)


By

(Unfolds  ``Knd  locl``  0  THEN  Auto)

---

Home Index