---

Step * 1 of Lemma not_rcv_locl


1. a : Id
2. l : IdLnk
3. tg : Id
4. rcv(l,tg) = (inr a ) ∈ (IdLnk × Id + Id)
⊢ False
BY
{ (ImpossibleEq Auto (-1) THEN Auto) }

---

Latex:



1.  a  :  Id
2.  l  :  IdLnk
3.  tg  :  Id
4.  rcv(l,tg)  =  (inr  a  )
\mvdash{}  False


By

(ImpossibleEq  Auto  (-1)  THEN  Auto)

---

Home Index