---

Step * of Lemma concat-lifting-list_wf

∀[B:Type]. ∀[n:ℕ]. ∀[m:ℕn + 1]. ∀[A:ℕn ⟶ Type]. ∀[bags:k:ℕn ⟶ bag(A k)]. ∀[g:funtype(n - m;λx.(A (x + m));bag(B))].
  (concat-lifting-list(n;bags) m g ∈ bag(B))
BY
{ ((UnivCD THENA Auto')
   THEN Unfold `concat-lifting-list` 0
   THEN Reduce 0
   THEN (BLemma `bag-union_wf` THENA Auto)
   THEN (BLemma `lifting-gen-list-rev_wf` THENA Auto)) }

---

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{}[g:funtype(n  -  m;\mlambda{}x.(A  (x  +  m));bag(B))].
    (concat-lifting-list(n;bags)  m  g  \mmember{}  bag(B))


By

---

Latex:
((UnivCD  THENA  Auto')
  THEN  Unfold  `concat-lifting-list`  0
  THEN  Reduce  0
  THEN  (BLemma  `bag-union\_wf`  THENA  Auto)
  THEN  (BLemma  `lifting-gen-list-rev\_wf`  THENA  Auto))

---

Home Index