---

Step * of Lemma bag-all_wf

∀[T:Type]. ∀[p:T ⟶ 𝔹]. ∀[bs:bag(T)].  (bag-all(x.p[x];bs) ∈ 𝔹)
BY
{ (ProveWfLemma THEN ((D 0 THEN Reduce 0) THEN Auto THEN (AutoBoolCase ⌜x⌝⋅ THEN AutoBoolCase ⌜y⌝⋅)⋅)⋅) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[p:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[bs:bag(T)].    (bag-all(x.p[x];bs)  \mmember{}  \mBbbB{})


By

---

Latex:
(ProveWfLemma
  THEN  ((D  0  THEN  Reduce  0)  THEN  Auto  THEN  (AutoBoolCase  \mkleeneopen{}x\mkleeneclose{}\mcdot{}  THEN  AutoBoolCase  \mkleeneopen{}y\mkleeneclose{}\mcdot{})\mcdot{})\mcdot{}
  )

---

Home Index