---

Step * 1 1 of Lemma lnk-decl-dom-not


1. l : IdLnk
2. d : Id List
3. d1 : tg:{tg:Id| (tg ∈ d)}  ─→ Type
4. a : Id
5. y : Id
6. (y ∈ d)
7. locl(a) = rcv(l,y) ∈ Knd
⊢ False
BY
{ ((FLemma `not_locl_rcv` [(-1)]) THEN Auto) }

---

Latex:



1.  l  :  IdLnk
2.  d  :  Id  List
3.  d1  :  tg:\{tg:Id|  (tg  \mmember{}  d)\}    {}\mrightarrow{}  Type
4.  a  :  Id
5.  y  :  Id
6.  (y  \mmember{}  d)
7.  locl(a)  =  rcv(l,y)
\mvdash{}  False


By

((FLemma  `not\_locl\_rcv`  [(-1)])  THEN  Auto)

---

Home Index