---

Step * 2 of Lemma lifting2-loc-lifting2-like


1. A : Type
2. B : Type
3. C : Type
4. f : Id ─→ A ─→ B ─→ C
5. i : Id
6. ∀as:bag(A). ∀bs:bag(B). ∀a:A. ∀b:B.
     (single-valued-bag(as;A)
     ⇒ single-valued-bag(bs;B)
     ⇒ a ↓∈ as
     ⇒ b ↓∈ bs
     ⇒ (↑bag-null(∪x∈as.∪x@0∈bs.{f i x x@0}) ⇐⇒ False))
7. as : bag(A)@i
⊢ ↑bag-null(∪x∈as.{})
BY
{ (Subst' ∪x∈as.{} ~ {} 0 THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  C  :  Type
4.  f  :  Id  {}\mrightarrow{}  A  {}\mrightarrow{}  B  {}\mrightarrow{}  C
5.  i  :  Id
6.  \mforall{}as:bag(A).  \mforall{}bs:bag(B).  \mforall{}a:A.  \mforall{}b:B.
          (single-valued-bag(as;A)
          {}\mRightarrow{}  single-valued-bag(bs;B)
          {}\mRightarrow{}  a  \mdownarrow{}\mmember{}  as
          {}\mRightarrow{}  b  \mdownarrow{}\mmember{}  bs
          {}\mRightarrow{}  (\muparrow{}bag-null(\mcup{}x\mmember{}as.\mcup{}x@0\mmember{}bs.\{f  i  x  x@0\})  \mLeftarrow{}{}\mRightarrow{}  False))
7.  as  :  bag(A)@i
\mvdash{}  \muparrow{}bag-null(\mcup{}x\mmember{}as.\{\})


By

---

Latex:
(Subst'  \mcup{}x\mmember{}as.\{\}  \msim{}  \{\}  0  THEN  Auto)

---

Home Index