---

Step * 1 2 of Lemma null-bag-size


1. T : Type
2. x : bag(T)
3. #(x) ≠ 0
⊢ bag-null(x) = ff
BY
{ AutoBoolCase ⌜bag-null(x)⌝⋅ }

1
1. T : Type
2. x : bag(T)
3. #(x) ≠ 0
4. x = {} ∈ bag(T)
⊢ tt = ff

---

Latex:

---

Latex:

1.  T  :  Type
2.  x  :  bag(T)
3.  \#(x)  \mneq{}  0
\mvdash{}  bag-null(x)  =  ff


By

---

Latex:
AutoBoolCase  \mkleeneopen{}bag-null(x)\mkleeneclose{}\mcdot{}

---

Home Index