---

Step * of Lemma concat-lifting-list-member

No Annotations
∀[B:Type]. ∀[n:ℕ]. ∀[m:ℕn + 1]. ∀[A:ℕn ⟶ Type]. ∀[bags:k:ℕn ⟶ bag(A k)]. ∀[f:funtype(n - m;λx.(A (x + m));bag(B))].
∀[b:B].
  (b ↓∈ concat-lifting-list(n;bags) m f
  ⇐⇒ ↓∃lst:k:{m..n-} ⟶ (A k). ((∀[k:{m..n-}]. lst k ↓∈ bags k) ∧ b ↓∈ uncurry-gen(n) m (λx.f) lst))
BY
{ ((UnivCD THENM D 0 THENM UnivCD)
   THENA (Auto
          THEN Try ((BLemma `concat-lifting-list_wf` THENA Auto)⋅)
          THEN Try (Complete ((InstLemma `uncurry-gen_wf2` [⌜bag(B)⌝; ⌜n⌝; ⌜m⌝; ⌜m⌝; ⌜A⌝; ⌜λx.f⌝]⋅ THEN Auto)))⋅
          THEN Try ((BLemma `lifting-gen-list-rev_wf` THEN Auto)))
   ) }

1
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));bag(B))
7. b : B
8. b ↓∈ concat-lifting-list(n;bags) m f
⊢ ↓∃lst:k:{m..n-} ⟶ (A k). ((∀[k:{m..n-}]. lst k ↓∈ bags k) ∧ b ↓∈ uncurry-gen(n) m (λx.f) lst)

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));bag(B))
7. b : B
8. ↓∃lst:k:{m..n-} ⟶ (A k). ((∀[k:{m..n-}]. lst k ↓∈ bags k) ∧ b ↓∈ uncurry-gen(n) m (λx.f) lst)
⊢ b ↓∈ concat-lifting-list(n;bags) m f

---

Latex:

---

Latex:
No  Annotations
\mforall{}[B:Type].  \mforall{}[n:\mBbbN{}].  \mforall{}[m:\mBbbN{}n  +  1].  \mforall{}[A:\mBbbN{}n  {}\mrightarrow{}  Type].  \mforall{}[bags:k:\mBbbN{}n  {}\mrightarrow{}  bag(A  k)].
\mforall{}[f:funtype(n  -  m;\mlambda{}x.(A  (x  +  m));bag(B))].  \mforall{}[b:B].
    (b  \mdownarrow{}\mmember{}  concat-lifting-list(n;bags)  m  f
    \mLeftarrow{}{}\mRightarrow{}  \mdownarrow{}\mexists{}lst:k:\{m..n\msupminus{}\}  {}\mrightarrow{}  (A  k)
                ((\mforall{}[k:\{m..n\msupminus{}\}].  lst  k  \mdownarrow{}\mmember{}  bags  k)  \mwedge{}  b  \mdownarrow{}\mmember{}  uncurry-gen(n)  m  (\mlambda{}x.f)  lst))


By

---

Latex:
((UnivCD  THENM  D  0  THENM  UnivCD)
  THENA  (Auto
                THEN  Try  ((BLemma  `concat-lifting-list\_wf`  THENA  Auto)\mcdot{})
                THEN  Try  (Complete  ((InstLemma  `uncurry-gen\_wf2`  [\mkleeneopen{}bag(B)\mkleeneclose{};  \mkleeneopen{}n\mkleeneclose{};  \mkleeneopen{}m\mkleeneclose{};  \mkleeneopen{}m\mkleeneclose{};  \mkleeneopen{}A\mkleeneclose{};  \mkleeneopen{}\mlambda{}x.f\mkleeneclose{}]\mcdot{}
                                                          THEN  Auto
                                                          )))\mcdot{}
                THEN  Try  ((BLemma  `lifting-gen-list-rev\_wf`  THEN  Auto)))
  )

---

Home Index