---

Step * of Lemma es-dt_wf

∀[l:IdLnk]. ∀[da:k:Knd fp-> Type].  (dt(l;da) ∈ tg:Id fp-> Type)
BY
{ ((Auto THEN Unfold `es-dt` 0)
   THEN MemCD
   THEN Try (Complete (Auto))
   THEN Reduce 0
   THEN Try (((MemCD THENA Auto) THEN AutoSplit))
   THEN (D 0 THENA Auto)
   THEN RepeatFor 2 (AutoSplit)
   THEN Auto) }

1
1. l : IdLnk
2. da : k:Knd fp-> Type
3. y : Knd@i
4. ↑isrcv(y)
5. lnk(y) = l ∈ IdLnk
6. True@i
⊢ rcv(l,tag(y)) = y ∈ Knd

---

Latex:


\mforall{}[l:IdLnk].  \mforall{}[da:k:Knd  fp->  Type].    (dt(l;da)  \mmember{}  tg:Id  fp->  Type)


By

((Auto  THEN  Unfold  `es-dt`  0)
  THEN  MemCD
  THEN  Try  (Complete  (Auto))
  THEN  Reduce  0
  THEN  Try  (((MemCD  THENA  Auto)  THEN  AutoSplit))
  THEN  (D  0  THENA  Auto)
  THEN  RepeatFor  2  (AutoSplit)
  THEN  Auto)

---

Home Index