---

Step * of Lemma concat-lifting-member

∀[B:Type]. ∀[n:ℕ]. ∀[A:ℕn ⟶ Type]. ∀[bags:k:ℕn ⟶ bag(A k)]. ∀[f:funtype(n;A;bag(B))]. ∀[b:B].
  (b ↓∈ concat-lifting(n;f;bags) ⇐⇒ ↓∃lst:k:ℕn ⟶ (A k). ((∀[k:ℕn]. lst k ↓∈ bags k) ∧ b ↓∈ uncurry-rev(n;f) lst))
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `concat-lifting` 0
   THEN (InstLemma `concat-lifting-list-member` [⌜B⌝; ⌜n⌝; ⌜0⌝; ⌜A⌝; ⌜bags⌝; ⌜f⌝; ⌜b⌝]⋅
         THENA (Auto
                THEN (Subst ⌜n - 0 ~ n⌝ 0⋅ THENA Auto)
                THEN Assert ⌜(λx.(A (x + 0))) = A ∈ (ℕn ⟶ Type)⌝⋅
                THEN Try (Complete (Auto))
                THEN Ext
                THEN Reduce 0
                THEN Auto)
         )
   THEN D (-1)
   THEN D 0
   THEN Auto
   THEN Try (Complete ((Unfold `uncurry-rev` 0 THEN Auto)))
   THEN Try (Complete ((BHyp (-2) THEN Unfold `uncurry-rev` (-1) THEN Auto)))
   THEN (BLemma `concat-lifting-list_wf` THENA Auto)
   THEN (Subst ⌜n - 0 ~ n⌝ 0⋅ THENA Auto)
   THEN Assert ⌜(λx.(A (x + 0))) = A ∈ (ℕn ⟶ Type)⌝⋅
   THEN Try (Complete (Auto))
   THEN Ext
   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))].  \mforall{}[b:B].
    (b  \mdownarrow{}\mmember{}  concat-lifting(n;f;bags)
    \mLeftarrow{}{}\mRightarrow{}  \mdownarrow{}\mexists{}lst:k:\mBbbN{}n  {}\mrightarrow{}  (A  k).  ((\mforall{}[k:\mBbbN{}n].  lst  k  \mdownarrow{}\mmember{}  bags  k)  \mwedge{}  b  \mdownarrow{}\mmember{}  uncurry-rev(n;f)  lst))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `concat-lifting`  0
  THEN  (InstLemma  `concat-lifting-list-member`  [\mkleeneopen{}B\mkleeneclose{};  \mkleeneopen{}n\mkleeneclose{};  \mkleeneopen{}0\mkleeneclose{};  \mkleeneopen{}A\mkleeneclose{};  \mkleeneopen{}bags\mkleeneclose{};  \mkleeneopen{}f\mkleeneclose{};  \mkleeneopen{}b\mkleeneclose{}]\mcdot{}
              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  (Auto))
                            THEN  Ext
                            THEN  Reduce  0
                            THEN  Auto)
              )
  THEN  D  (-1)
  THEN  D  0
  THEN  Auto
  THEN  Try  (Complete  ((Unfold  `uncurry-rev`  0  THEN  Auto)))
  THEN  Try  (Complete  ((BHyp  (-2)  THEN  Unfold  `uncurry-rev`  (-1)  THEN  Auto)))
  THEN  (BLemma  `concat-lifting-list\_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  (Auto))
  THEN  Ext
  THEN  Reduce  0
  THEN  Auto)

---

Home Index