---

Step * of Lemma lnk-decl-cap2

∀[l1,l2:IdLnk]. ∀[dt:tg:Id fp-> Type]. ∀[tg:Id]. ∀[T:Type].
  (lnk-decl(l1;dt)(rcv(l2,tg))?T ~ if l1 = l2 then dt(tg)?T else T fi )
BY
{ (((UnivCD THENA Auto) THEN SplitOnConclITE) THENA Auto) }

1
.....truecase..... 
1. l1 : IdLnk
2. l2 : IdLnk
3. dt : tg:Id fp-> Type
4. tg : Id
5. T : Type
6. l1 = l2 ∈ IdLnk
⊢ lnk-decl(l1;dt)(rcv(l2,tg))?T ~ dt(tg)?T

2
.....falsecase..... 
1. l1 : IdLnk
2. l2 : IdLnk
3. dt : tg:Id fp-> Type
4. tg : Id
5. T : Type
6. ¬(l1 = l2 ∈ IdLnk)
⊢ lnk-decl(l1;dt)(rcv(l2,tg))?T ~ T

---

Latex:


\mforall{}[l1,l2:IdLnk].  \mforall{}[dt:tg:Id  fp->  Type].  \mforall{}[tg:Id].  \mforall{}[T:Type].
    (lnk-decl(l1;dt)(rcv(l2,tg))?T  \msim{}  if  l1  =  l2  then  dt(tg)?T  else  T  fi  )


By

(((UnivCD  THENA  Auto)  THEN  SplitOnConclITE)  THENA  Auto)

---

Home Index