---

Step * of Lemma lifting2-loc-lifting2-like

∀[A,B,C:Type]. ∀[f:Id ─→ A ─→ B ─→ C]. ∀[i:Id].  lifting2-like(A;B;λas,bs. lifting2-loc(f;i;as;bs))
BY
{ ((UnivCD THENA Auto)
   THEN (RepUR ``lifting2-like lifting2-loc 
             lifting-loc-gen-rev lifting-gen-rev`` 0⋅
         THEN RepeatFor 3 ((RecUnfold `lifting-gen-list-rev` 0 THEN Reduce 0))
         )⋅
   THEN Auto) }

1
1. A : Type
2. B : Type
3. C : Type
4. f : Id ─→ A ─→ B ─→ C
5. i : Id
6. as : bag(A)@i
7. bs : bag(B)@i
8. a : A@i
9. b : B@i
10. single-valued-bag(as;A)@i
11. single-valued-bag(bs;B)@i
12. a ↓∈ as@i
13. b ↓∈ bs@i
14. ↑bag-null(∪x∈as.∪x@0∈bs.{f i x x@0})@i
⊢ False

2
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.{})

---

Latex:

---

Latex:
\mforall{}[A,B,C:Type].  \mforall{}[f:Id  {}\mrightarrow{}  A  {}\mrightarrow{}  B  {}\mrightarrow{}  C].  \mforall{}[i:Id].    lifting2-like(A;B;\mlambda{}as,bs.  lifting2-loc(f;i;as;bs))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (RepUR  ``lifting2-like  lifting2-loc 
                      lifting-loc-gen-rev  lifting-gen-rev``  0\mcdot{}
              THEN  RepeatFor  3  ((RecUnfold  `lifting-gen-list-rev`  0  THEN  Reduce  0))
              )\mcdot{}
  THEN  Auto)

---

Home Index