---

Step * 1 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
⊢ (d3 y1) = (d5 y1) ∈ Type
BY
{ AllHyps h.(((Repeat ((Unfolds ``fpf-compatible fpf-dom fpf-ap`` h THEN Reduce h)) THEN BHyp  h) THENA Auto)
             THEN RWO "assert-deq-member" 0
             THEN Auto)  }

---

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{}  (d3  y1)  =  (d5  y1)


By

AllHyps  h.(((Repeat  ((Unfolds  ``fpf-compatible  fpf-dom  fpf-ap``  h  THEN  Reduce  h))  THEN  BHyp    h)
                        THENA  Auto
                        )
                      THEN  RWO  "assert-deq-member"  0
                      THEN  Auto) 

---

Home Index