---

Step * 2 of Lemma lnk-decl-dom-implies


1. y : Id
2. l : IdLnk
3. dt : x:Id fp-> Type
4. ↑locl(y) ∈ dom(lnk-decl(l;dt))
⊢ False c∧ (↑snd(⊥) ∈ dom(dt))
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{}  False  c\mwedge{}  (\muparrow{}snd(\mbot{})  \mmember{}  dom(dt))


By

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

---

Home Index