---

Step * 2 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) ⇒ <d, d3> || <d4, d5>
8. x : Knd@i
9. y : Id
10. (y ∈ d)
11. x = rcv(l1,y) ∈ Knd
12. y1 : Id
13. (y1 ∈ d4)
14. x = rcv(l2,y1) ∈ Knd
⊢ l1 = l2 ∈ IdLnk
BY
{ ((HypSubst' (-4) (-1)) THEN (FLemma `rcv_one_one` [(-1)]) 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)  {}\mRightarrow{}  <d,  d3>  ||  <d4,  d5>
8.  x  :  Knd@i
9.  y  :  Id
10.  (y  \mmember{}  d)
11.  x  =  rcv(l1,y)
12.  y1  :  Id
13.  (y1  \mmember{}  d4)
14.  x  =  rcv(l2,y1)
\mvdash{}  l1  =  l2


By

((HypSubst'  (-4)  (-1))  THEN  (FLemma  `rcv\_one\_one`  [(-1)])  THEN  Auto)

---

Home Index