---

Step * of Lemma concat-lifting1_wf

∀[A,B:Type]. ∀[f:A ⟶ bag(B)]. ∀[b:bag(A)].  (concat-lifting1(f;b) ∈ bag(B))
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `concat-lifting1` 0
   THEN (InstLemma `concat-lifting_wf` [⌜B⌝; ⌜1⌝; ⌜λx.A⌝; ⌜λx.b⌝; ⌜f⌝]⋅ THENA Auto)
   THEN Try (Complete (Auto))
   THEN Unfold `funtype` 0
   THEN RWO "primrec-unroll" 0
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[f:A  {}\mrightarrow{}  bag(B)].  \mforall{}[b:bag(A)].    (concat-lifting1(f;b)  \mmember{}  bag(B))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `concat-lifting1`  0
  THEN  (InstLemma  `concat-lifting\_wf`  [\mkleeneopen{}B\mkleeneclose{};  \mkleeneopen{}1\mkleeneclose{};  \mkleeneopen{}\mlambda{}x.A\mkleeneclose{};  \mkleeneopen{}\mlambda{}x.b\mkleeneclose{};  \mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Try  (Complete  (Auto))
  THEN  Unfold  `funtype`  0
  THEN  RWO  "primrec-unroll"  0
  THEN  Reduce  0
  THEN  Auto)

---

Home Index