---

Step * of Lemma lifting-member-simple

∀[B:Type]. ∀[n:ℕ]. ∀[A:ℕn ⟶ Type]. ∀[bags:k:ℕn ⟶ bag(A k)]. ∀[f:funtype(n;A;B)]. ∀[b:B].
  (b ↓∈ lifting-gen-rev(n;f;bags)
  ⇐⇒ ↓∃lst:k:ℕn ⟶ (A k). ((∀[k:ℕn]. lst k ↓∈ bags k) ∧ ((uncurry-rev(n;f) lst) = b ∈ B)))
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `lifting-gen-rev` 0
   THEN Unfold `uncurry-rev` 0
   THEN (InstLemma `lifting-member` [⌜B⌝; ⌜n⌝; ⌜0⌝; ⌜A⌝; ⌜bags⌝; ⌜f⌝; ⌜b⌝]⋅ THENA Auto)
   THEN Try (Complete (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
   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;B)].  \mforall{}[b:B].
    (b  \mdownarrow{}\mmember{}  lifting-gen-rev(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{}  ((uncurry-rev(n;f)  lst)  =  b)))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `lifting-gen-rev`  0
  THEN  Unfold  `uncurry-rev`  0
  THEN  (InstLemma  `lifting-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  Try  (Complete  (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
  THEN  Reduce  0
  THEN  Auto)

---

Home Index