---

Step * of Lemma lifting1-loc-lifting-like

∀[A,B:Type]. ∀[f:Id ─→ A ─→ B]. ∀[i:Id].  lifting-like(A;λa.lifting1-loc(f;i;a))
BY
{ (RepUR ``lifting-like lifting1-loc lifting-loc-gen-rev lifting-gen-rev`` 0⋅
   THEN RepeatFor 2 ((RecUnfold `lifting-gen-list-rev` 0 THEN Reduce 0))
   THEN Auto) }

1
1. A : Type
2. B : Type
3. f : Id ─→ A ─→ B
4. i : Id
5. as : bag(A)@i
6. x : A@i
7. single-valued-bag(as;A)@i
8. x ↓∈ as@i
9. ↑bag-null(∪x∈as.{f i x})@i
⊢ False

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[f:Id  {}\mrightarrow{}  A  {}\mrightarrow{}  B].  \mforall{}[i:Id].    lifting-like(A;\mlambda{}a.lifting1-loc(f;i;a))


By

---

Latex:
(RepUR  ``lifting-like  lifting1-loc  lifting-loc-gen-rev  lifting-gen-rev``  0\mcdot{}
  THEN  RepeatFor  2  ((RecUnfold  `lifting-gen-list-rev`  0  THEN  Reduce  0))
  THEN  Auto)

---

Home Index