---

Step * of Lemma bag-member-lifting-2

∀[C,B,A:Type]. ∀[f:A ⟶ B ⟶ C]. ∀[as:bag(A)]. ∀[bs:bag(B)]. ∀[c:C].
  uiff(c ↓∈ lifting-2(f) as bs;↓∃a:A. ∃b:B. (a ↓∈ as ∧ b ↓∈ bs ∧ (c = (f a b) ∈ C)))
BY
{ ((UnivCD THENA Auto) THEN D 0 THEN Auto) }

1
1. C : Type
2. B : Type
3. A : Type
4. f : A ⟶ B ⟶ C
5. as : bag(A)
6. bs : bag(B)
7. c : C
8. c ↓∈ lifting-2(f) as bs
⊢ ↓∃a:A. ∃b:B. (a ↓∈ as ∧ b ↓∈ bs ∧ (c = (f a b) ∈ C))

2
1. C : Type
2. B : Type
3. A : Type
4. f : A ⟶ B ⟶ C
5. as : bag(A)
6. bs : bag(B)
7. c : C
8. ↓∃a:A. ∃b:B. (a ↓∈ as ∧ b ↓∈ bs ∧ (c = (f a b) ∈ C))
⊢ c ↓∈ lifting-2(f) as bs

---

Latex:

---

Latex:
\mforall{}[C,B,A:Type].  \mforall{}[f:A  {}\mrightarrow{}  B  {}\mrightarrow{}  C].  \mforall{}[as:bag(A)].  \mforall{}[bs:bag(B)].  \mforall{}[c:C].
    uiff(c  \mdownarrow{}\mmember{}  lifting-2(f)  as  bs;\mdownarrow{}\mexists{}a:A.  \mexists{}b:B.  (a  \mdownarrow{}\mmember{}  as  \mwedge{}  b  \mdownarrow{}\mmember{}  bs  \mwedge{}  (c  =  (f  a  b))))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  D  0  THEN  Auto)

---

Home Index