---

Step * of Lemma lnk-decl-cap

∀[l:IdLnk]. ∀[dt:tg:Id fp-> Type]. ∀[tg:Id]. ∀[T:Type].  (lnk-decl(l;dt)(rcv(l,tg))?T ~ dt(tg)?T)
BY
{ (UnivCD THENA Auto) }

1
1. l : IdLnk
2. dt : tg:Id fp-> Type
3. tg : Id
4. T : Type
⊢ lnk-decl(l;dt)(rcv(l,tg))?T ~ dt(tg)?T

---

Latex:


\mforall{}[l:IdLnk].  \mforall{}[dt:tg:Id  fp->  Type].  \mforall{}[tg:Id].  \mforall{}[T:Type].    (lnk-decl(l;dt)(rcv(l,tg))?T  \msim{}  dt(tg)?T)


By

(UnivCD  THENA  Auto)

---

Home Index