---

Step * 2 of Lemma lnk-decl-ap


1. y : Id
2. l : IdLnk
3. dt : x:Id fp-> Type
4. ↑locl(y) ∈ dom(lnk-decl(l;dt))
⊢ lnk-decl(l;dt)(locl(y)) ~ dt(snd(⊥))
BY
{ ((RWO "lnk-decl-dom-not" (-1)) THEN (Reduce (-1)) THEN Auto) }

---

Latex:



1.  y  :  Id
2.  l  :  IdLnk
3.  dt  :  x:Id  fp->  Type
4.  \muparrow{}locl(y)  \mmember{}  dom(lnk-decl(l;dt))
\mvdash{}  lnk-decl(l;dt)(locl(y))  \msim{}  dt(snd(\mbot{}))


By

((RWO  "lnk-decl-dom-not"  (-1))  THEN  (Reduce  (-1))  THEN  Auto)

---

Home Index