---

Step * 1 1 1 of Lemma lnk-decls-compatible


1. l1 : IdLnk
2. l2 : IdLnk
3. d : Id List
4. d3 : tg:{tg:Id| (tg ∈ d)}  ─→ Type
5. d4 : Id List
6. d5 : tg:{tg:Id| (tg ∈ d4)}  ─→ Type
7. l1 = l2 ∈ IdLnk
8. <d, d3> || <d4, d5>
9. x : Knd@i
10. y : Id
11. (y ∈ d)
12. x = rcv(l2,y) ∈ Knd
13. y1 : Id
14. (y1 ∈ d4)
15. x = rcv(l2,y1) ∈ Knd
⊢ lnk-decl(l2;<d, d3>)(x) = lnk-decl(l2;<d4, d5>)(x) ∈ Type
BY
{ ((HypSubst' (-1) 0) THEN Repeat ((Unfolds ``rcv lnk-decl fpf-ap`` 0 THEN Reduce 0))) }

1
1. l1 : IdLnk
2. l2 : IdLnk
3. d : Id List
4. d3 : tg:{tg:Id| (tg ∈ d)}  ─→ Type
5. d4 : Id List
6. d5 : tg:{tg:Id| (tg ∈ d4)}  ─→ Type
7. l1 = l2 ∈ IdLnk
8. <d, d3> || <d4, d5>
9. x : Knd@i
10. y : Id
11. (y ∈ d)
12. x = rcv(l2,y) ∈ Knd
13. y1 : Id
14. (y1 ∈ d4)
15. x = rcv(l2,y1) ∈ Knd
⊢ (d3 y1) = (d5 y1) ∈ Type

---

Latex:



1.  l1  :  IdLnk
2.  l2  :  IdLnk
3.  d  :  Id  List
4.  d3  :  tg:\{tg:Id|  (tg  \mmember{}  d)\}    {}\mrightarrow{}  Type
5.  d4  :  Id  List
6.  d5  :  tg:\{tg:Id|  (tg  \mmember{}  d4)\}    {}\mrightarrow{}  Type
7.  l1  =  l2
8.  <d,  d3>  ||  <d4,  d5>
9.  x  :  Knd@i
10.  y  :  Id
11.  (y  \mmember{}  d)
12.  x  =  rcv(l2,y)
13.  y1  :  Id
14.  (y1  \mmember{}  d4)
15.  x  =  rcv(l2,y1)
\mvdash{}  lnk-decl(l2;<d,  d3>)(x)  =  lnk-decl(l2;<d4,  d5>)(x)


By

((HypSubst'  (-1)  0)  THEN  Repeat  ((Unfolds  ``rcv  lnk-decl  fpf-ap``  0  THEN  Reduce  0)))

---

Home Index