---

Step * of Lemma lifting-member

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

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


By

---

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

---

Home Index