---

Step * 1 2 1 1 of Lemma lnk-decl-cap


1. l : IdLnk
2. d : Id List
3. d1 : tg:{tg:Id| (tg ∈ d)}  ─→ Type
4. tg : Id
5. T : Type
6. (rcv(l,tg) ∈ map(λtg.rcv(l,tg);d))
⊢ (tg ∈ d)
BY
{ ((RWO "member_map" (-1))
   THEN (Reduce (-1))
   THEN Auto
   THEN ExRepD
   THEN (FLemma `rcv_one_one` [(-1)])
   THEN Auto
   THEN (HypSubst' (-1) 0)
   THEN Auto) }

---

Latex:



1.  l  :  IdLnk
2.  d  :  Id  List
3.  d1  :  tg:\{tg:Id|  (tg  \mmember{}  d)\}    {}\mrightarrow{}  Type
4.  tg  :  Id
5.  T  :  Type
6.  (rcv(l,tg)  \mmember{}  map(\mlambda{}tg.rcv(l,tg);d))
\mvdash{}  (tg  \mmember{}  d)


By

((RWO  "member\_map"  (-1))
  THEN  (Reduce  (-1))
  THEN  Auto
  THEN  ExRepD
  THEN  (FLemma  `rcv\_one\_one`  [(-1)])
  THEN  Auto
  THEN  (HypSubst'  (-1)  0)
  THEN  Auto)

---

Home Index