---

Step * of Lemma lnk-decl-dom-implies

∀[k:Knd]. ∀[l:IdLnk]. ∀[dt:x:Id fp-> Type].  {(↑isrcv(k)) c∧ (↑tag(k) ∈ dom(dt))} supposing ↑k ∈ dom(lnk-decl(l;dt))
BY
{ ((UnivCD THENA Auto) THEN KindCases) }

1
1. x1 : IdLnk
2. x2 : Id
3. l : IdLnk
4. dt : x:Id fp-> Type
5. ↑rcv(x1,x2) ∈ dom(lnk-decl(l;dt))
⊢ True c∧ (↑x2 ∈ dom(dt))

2
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))

---

Latex:


\mforall{}[k:Knd].  \mforall{}[l:IdLnk].  \mforall{}[dt:x:Id  fp->  Type].
    \{(\muparrow{}isrcv(k))  c\mwedge{}  (\muparrow{}tag(k)  \mmember{}  dom(dt))\}  supposing  \muparrow{}k  \mmember{}  dom(lnk-decl(l;dt))


By

((UnivCD  THENA  Auto)  THEN  KindCases)

---

Home Index