---

Step * 2 of Lemma lifting-member


1. B : Type
2. n : ℕ
3. m : ℕn + 1
4. A : ℕn ⟶ Type
5. bags : k:ℕn ⟶ bag(A k)
6. f : funtype(n - m;λx.(A (x + m));B)
7. b : B
8. ↓∃lst:k:{m..n-} ⟶ (A k). ((∀[k:{m..n-}]. lst k ↓∈ bags k) ∧ ((uncurry-gen(n) m (λx.f) lst) = b ∈ B))
⊢ b ↓∈ lifting-gen-list-rev(n;bags) m f
BY
{ (D (-1) THEN Unhide⋅ THEN Auto) }

1
.....wf..... 
1. B : Type
2. n : ℕ
3. m : ℕn + 1
4. A : ℕn ⟶ Type
5. bags : k:ℕn ⟶ bag(A k)
6. f : funtype(n - m;λx.(A (x + m));B)
7. b : B
8. ∃lst:k:{m..n-} ⟶ (A k). ((∀[k:{m..n-}]. lst k ↓∈ bags k) ∧ ((uncurry-gen(n) m (λx.f) lst) = b ∈ B))
⊢ lifting-gen-list-rev(n;bags) m f ∈ bag(B)

2
1. B : Type
2. n : ℕ
3. m : ℕn + 1
4. A : ℕn ⟶ Type
5. bags : k:ℕn ⟶ bag(A k)
6. f : funtype(n - m;λx.(A (x + m));B)
7. b : B
8. ∃lst:k:{m..n-} ⟶ (A k). ((∀[k:{m..n-}]. lst k ↓∈ bags k) ∧ ((uncurry-gen(n) m (λx.f) lst) = b ∈ B))
⊢ b ↓∈ lifting-gen-list-rev(n;bags) m f

---

Latex:

---

Latex:

1.  B  :  Type
2.  n  :  \mBbbN{}
3.  m  :  \mBbbN{}n  +  1
4.  A  :  \mBbbN{}n  {}\mrightarrow{}  Type
5.  bags  :  k:\mBbbN{}n  {}\mrightarrow{}  bag(A  k)
6.  f  :  funtype(n  -  m;\mlambda{}x.(A  (x  +  m));B)
7.  b  :  B
8.  \mdownarrow{}\mexists{}lst:k:\{m..n\msupminus{}\}  {}\mrightarrow{}  (A  k).  ((\mforall{}[k:\{m..n\msupminus{}\}].  lst  k  \mdownarrow{}\mmember{}  bags  k)  \mwedge{}  ((uncurry-gen(n)  m  (\mlambda{}x.f)  lst)  =  b))
\mvdash{}  b  \mdownarrow{}\mmember{}  lifting-gen-list-rev(n;bags)  m  f


By

---

Latex:
(D  (-1)  THEN  Unhide\mcdot{}  THEN  Auto)

---

Home Index