---

Step * of Lemma lnk-decl-dom-join

∀[l:IdLnk]. ∀[k:Knd]. ∀[dt1,dt2:tg:Id fp-> Type].
  (k ∈ dom(lnk-decl(l;dt1 ⊕ dt2)) ~ k ∈ dom(lnk-decl(l;dt1)) ∨bk ∈ dom(lnk-decl(l;dt2)))
BY
{ (Auto THEN (BLemma `iff_imp_equal_bool` THENA Auto) THEN RepUR ``lnk-decl fpf-dom`` 0) }

1
1. l : IdLnk
2. k : Knd
3. dt1 : tg:Id fp-> Type
4. dt2 : tg:Id fp-> Type
⊢ ↑k ∈b map(λtg.rcv(l,tg);fst(dt1 ⊕ dt2))) ⇐⇒ ↑(k ∈b map(λtg.rcv(l,tg);fst(dt1))) ∨bk ∈b map(λtg.rcv(l,tg);fst(dt2))))

---

Latex:


\mforall{}[l:IdLnk].  \mforall{}[k:Knd].  \mforall{}[dt1,dt2:tg:Id  fp->  Type].
    (k  \mmember{}  dom(lnk-decl(l;dt1  \moplus{}  dt2))  \msim{}  k  \mmember{}  dom(lnk-decl(l;dt1))  \mvee{}\msubb{}k  \mmember{}  dom(lnk-decl(l;dt2)))


By

(Auto  THEN  (BLemma  `iff\_imp\_equal\_bool`  THENA  Auto)  THEN  RepUR  ``lnk-decl  fpf-dom``  0)

---

Home Index