---

Step * 1 of Lemma lnk-decl-dom


1. l : IdLnk
2. d : Id List
3. d1 : tg:{tg:Id| (tg ∈ d)}  ─→ Type
4. tg : Id
⊢ rcv(l,tg) ∈b map(λtg.rcv(l,tg);d)) = tg ∈b d)
BY
{ (BLemma `iff_imp_equal_bool`
   THEN Auto
   THEN (All (RWO "assert-deq-member"))
   THEN Auto
   THEN (All (RWO "member_map"))
   THEN Auto
   THEN All Reduce
   THEN ExRepD) }

1
1. l : IdLnk
2. d : Id List
3. d1 : tg:{tg:Id| (tg ∈ d)}  ─→ Type
4. tg : Id
5. y : Id
6. (y ∈ d)
7. rcv(l,tg) = rcv(l,y) ∈ Knd
⊢ (tg ∈ d)

---

Latex:



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


By

(BLemma  `iff\_imp\_equal\_bool`
  THEN  Auto
  THEN  (All  (RWO  "assert-deq-member"))
  THEN  Auto
  THEN  (All  (RWO  "member\_map"))
  THEN  Auto
  THEN  All  Reduce
  THEN  ExRepD)

---

Home Index