---

Step * of Lemma bag-member-evidence

∀[T:Type]. ∀[b:bag(T)]. ∀[x:T].  Ax ∈ x ↓∈ b supposing x ↓∈ b
BY
{ (Auto THEN ProveTrivialWitness) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[b:bag(T)].  \mforall{}[x:T].    Ax  \mmember{}  x  \mdownarrow{}\mmember{}  b  supposing  x  \mdownarrow{}\mmember{}  b


By

---

Latex:
(Auto  THEN  ProveTrivialWitness)

---

Home Index