---

Step * of Lemma concat-lifting_wf

∀[B:Type]. ∀[n:ℕ]. ∀[A:ℕn ⟶ Type]. ∀[bags:k:ℕn ⟶ bag(A k)]. ∀[f:funtype(n;A;bag(B))].
  (concat-lifting(n;f;bags) ∈ bag(B))
BY
{ (ProveWfLemma
   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)
   THEN (Subst ⌜n - 0 ~ n⌝ 0⋅ THENA Auto)
   THEN Assert ⌜(λx.(A (x + 0))) = A ∈ (ℕn ⟶ Type)⌝⋅
   THEN Try (Complete ((RWO "-1" 0 THEN Auto)))
   THEN (Ext THENA Auto)
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[B:Type].  \mforall{}[n:\mBbbN{}].  \mforall{}[A:\mBbbN{}n  {}\mrightarrow{}  Type].  \mforall{}[bags:k:\mBbbN{}n  {}\mrightarrow{}  bag(A  k)].  \mforall{}[f:funtype(n;A;bag(B))].
    (concat-lifting(n;f;bags)  \mmember{}  bag(B))


By

---

Latex:
(ProveWfLemma
  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)
  THEN  (Subst  \mkleeneopen{}n  -  0  \msim{}  n\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  Assert  \mkleeneopen{}(\mlambda{}x.(A  (x  +  0)))  =  A\mkleeneclose{}\mcdot{}
  THEN  Try  (Complete  ((RWO  "-1"  0  THEN  Auto)))
  THEN  (Ext  THENA  Auto)
  THEN  Reduce  0
  THEN  Auto)

---

Home Index