---

Step * of Lemma lnk-decl-ap

∀[k:Knd]. ∀[l:IdLnk]. ∀[dt:x:Id fp-> Type].  lnk-decl(l;dt)(k) ~ dt(tag(k)) 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))
⊢ lnk-decl(l;dt)(rcv(x1,x2)) ~ dt(x2)

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

---

Latex:


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


By

((UnivCD  THENA  Auto)  THEN  KindCases)

---

Home Index