---

Step * of Lemma lifting-0_wf

∀[B:Type]. ∀[b:B].  (lifting-0(b) ∈ bag(B))
BY
{ (ProveWfLemma
   THEN InstLemma `lifting-gen-rev_wf` [⌜B⌝; ⌜0⌝; ⌜λn.[][n]⌝; ⌜λn.[][n]⌝; ⌜b⌝]⋅
   THEN Auto
   THEN Unfold `funtype` 0
   THEN Unfold `primrec` 0
   THEN (RWO "ycomb-unroll" 0 THENA Auto)
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[B:Type].  \mforall{}[b:B].    (lifting-0(b)  \mmember{}  bag(B))


By

---

Latex:
(ProveWfLemma
  THEN  InstLemma  `lifting-gen-rev\_wf`  [\mkleeneopen{}B\mkleeneclose{};  \mkleeneopen{}0\mkleeneclose{};  \mkleeneopen{}\mlambda{}n.[][n]\mkleeneclose{};  \mkleeneopen{}\mlambda{}n.[][n]\mkleeneclose{};  \mkleeneopen{}b\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  Unfold  `funtype`  0
  THEN  Unfold  `primrec`  0
  THEN  (RWO  "ycomb-unroll"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  Auto)

---

Home Index