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. IdLnk
2. 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