---

Step * of Lemma bag-member-lifting-loc-2

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

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

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

---

Latex:

---

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


By

---

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

---

Home Index