---

Step * 1 of Lemma lnk-decl-cap


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
BY
{ (((((Unfold `fpf-cap` 0 THEN SplitOnConclITE) THENA Auto) THEN SplitOnConclITE) THENA Auto) THEN Try (Trivial)) }

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

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

3
.....truecase..... 
1. l : IdLnk
2. dt : tg:Id fp-> Type
3. tg : Id
4. T : Type
5. ¬↑rcv(l,tg) ∈ dom(lnk-decl(l;dt))
6. ↑tg ∈ dom(dt)
⊢ T ~ dt(tg)

---

Latex:



1.  l  :  IdLnk
2.  dt  :  tg:Id  fp->  Type
3.  tg  :  Id
4.  T  :  Type
\mvdash{}  lnk-decl(l;dt)(rcv(l,tg))?T  \msim{}  dt(tg)?T


By

(((((Unfold  `fpf-cap`  0  THEN  SplitOnConclITE)  THENA  Auto)  THEN  SplitOnConclITE)  THENA  Auto)
  THEN  Try  (Trivial)
  )

---

Home Index