---

Step * 1 1 1 1 1 1 of Lemma lnk-decl-compatible-single

.....antecedent..... 
1. l : IdLnk
2. d : Id List
3. d1 : tg:{tg:Id| (tg ∈ d)}  ─→ Type
4. knd : Knd
5. T : Type
6. x : Knd@i
7. y : Id
8. (y ∈ d)
9. x = rcv(l,y) ∈ Knd
10. x = knd ∈ Knd
⊢ ↑isrcv(knd)
BY
{ ((RevHypSubst' (-1) 0) THEN (HypSubst' (-2) 0) THEN Unfolds ``isrcv rcv`` 0 THEN Reduce 0 THEN Auto) }

---

Latex:


.....antecedent..... 
1.  l  :  IdLnk
2.  d  :  Id  List
3.  d1  :  tg:\{tg:Id|  (tg  \mmember{}  d)\}    {}\mrightarrow{}  Type
4.  knd  :  Knd
5.  T  :  Type
6.  x  :  Knd@i
7.  y  :  Id
8.  (y  \mmember{}  d)
9.  x  =  rcv(l,y)
10.  x  =  knd
\mvdash{}  \muparrow{}isrcv(knd)


By

((RevHypSubst'  (-1)  0)  THEN  (HypSubst'  (-2)  0)  THEN  Unfolds  ``isrcv  rcv``  0  THEN  Reduce  0  THEN  Auto)

---

Home Index