---

Step * of Lemma concat-lifting2_wf

∀[A,B,C:Type]. ∀[f:A ⟶ B ⟶ bag(C)]. ∀[abag:bag(A)]. ∀[bbag:bag(B)].  (concat-lifting2(f;abag;bbag) ∈ bag(C))
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `concat-lifting2` 0
   THEN InstLemma `concat-lifting_wf` [⌜C⌝; ⌜2⌝; ⌜λn.[A; B][n]⌝; ⌜λn.[abag; bbag][n]⌝; ⌜f⌝]⋅
   THEN Try (Complete (Auto'))
   THEN Try (Complete (((MemCD THENA Auto) THEN IntSegCases (-1) THEN Reduce 0 THEN Auto)))
   THEN Unfold `funtype` 0
   THEN RWO "primrec-unroll" 0
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B,C:Type].  \mforall{}[f:A  {}\mrightarrow{}  B  {}\mrightarrow{}  bag(C)].  \mforall{}[abag:bag(A)].  \mforall{}[bbag:bag(B)].
    (concat-lifting2(f;abag;bbag)  \mmember{}  bag(C))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `concat-lifting2`  0
  THEN  InstLemma  `concat-lifting\_wf`  [\mkleeneopen{}C\mkleeneclose{};  \mkleeneopen{}2\mkleeneclose{};  \mkleeneopen{}\mlambda{}n.[A;  B][n]\mkleeneclose{};  \mkleeneopen{}\mlambda{}n.[abag;  bbag][n]\mkleeneclose{};  \mkleeneopen{}f\mkleeneclose{}]\mcdot{}
  THEN  Try  (Complete  (Auto'))
  THEN  Try  (Complete  (((MemCD  THENA  Auto)  THEN  IntSegCases  (-1)  THEN  Reduce  0  THEN  Auto)))
  THEN  Unfold  `funtype`  0
  THEN  RWO  "primrec-unroll"  0
  THEN  Reduce  0
  THEN  Auto)

---

Home Index