---

Step * of Lemma lnk-decl-compatible-single

∀[l:IdLnk]. ∀[dt:tg:Id fp-> Type]. ∀[knd:Knd]. ∀[T:Type].
  lnk-decl(l;dt) || knd : T 
  supposing (↑isrcv(knd)) ⇒ (↑lnk(knd) = l) ⇒ (↑tag(knd) ∈ dom(dt)) ⇒ (T = dt(tag(knd)) ∈ Type)
BY
{ (Unfold `fpf-compatible` 0 THEN Auto THEN (RWW "fpf-single-dom" (-1)) THEN Auto THEN HypSubst' (-1) 0 THEN Reduce 0) }

1
1. l : IdLnk
2. dt : tg:Id fp-> Type
3. knd : Knd
4. T : Type
5. (↑isrcv(knd)) ⇒ (↑lnk(knd) = l) ⇒ (↑tag(knd) ∈ dom(dt)) ⇒ (T = dt(tag(knd)) ∈ Type)
6. x : Knd@i
7. ↑x ∈ dom(lnk-decl(l;dt))@i
8. x = knd ∈ Knd
⊢ lnk-decl(l;dt)(knd) = T ∈ Type

---

Latex:


\mforall{}[l:IdLnk].  \mforall{}[dt:tg:Id  fp->  Type].  \mforall{}[knd:Knd].  \mforall{}[T:Type].
    lnk-decl(l;dt)  ||  knd  :  T 
    supposing  (\muparrow{}isrcv(knd))  {}\mRightarrow{}  (\muparrow{}lnk(knd)  =  l)  {}\mRightarrow{}  (\muparrow{}tag(knd)  \mmember{}  dom(dt))  {}\mRightarrow{}  (T  =  dt(tag(knd)))


By

(Unfold  `fpf-compatible`  0
  THEN  Auto
  THEN  (RWW  "fpf-single-dom"  (-1))
  THEN  Auto
  THEN  HypSubst'  (-1)  0
  THEN  Reduce  0)

---

Home Index