---

Step * 1 of Lemma empty-bag-iff-no-member


1. T : Type
2. bs : bag(T)
3. bs = {} ∈ bag(T)
4. x : T
⊢ ¬x ↓∈ bs
BY
{ ((D 0 THENA Auto) THEN (HypSubst' 3 (-1) THENA Auto) THEN FLemma `bag-member-empty` [-1] THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  bs  :  bag(T)
3.  bs  =  \{\}
4.  x  :  T
\mvdash{}  \mneg{}x  \mdownarrow{}\mmember{}  bs


By

---

Latex:
((D  0  THENA  Auto)  THEN  (HypSubst'  3  (-1)  THENA  Auto)  THEN  FLemma  `bag-member-empty`  [-1]  THEN  Auto)

---

Home Index