---

Step * of Lemma concat-lifting1-loc_wf

∀[A,B:Type]. ∀[f:Id ─→ A ─→ bag(B)]. ∀[b:bag(A)]. ∀[l:Id].  (concat-lifting1-loc(f;b;l) ∈ bag(B))
BY
{ (ProveWfLemma
   THEN (InstLemma `concat-lifting-loc_wf` [⌈B⌉; ⌈1⌉; ⌈λx.A⌉; ⌈λx.b⌉; ⌈l⌉; ⌈f⌉]⋅ THENA Auto)
   THEN Try (Complete (Auto))
   THEN Unfold `funtype` 0
   THEN Repeat (((RWO "primrec-unroll" 0 THENM Reduce 0) THEN Auto))) }

---

Latex:

---

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


By

---

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

---

Home Index