---

Step * 1 1 of Lemma null-bag-size


1. T : Type
2. x : bag(T)
3. #(x) = 0 ∈ ℤ
⊢ bag-null(x) = tt
BY
{ (InstLemma `bag-size-zero` [⌜T⌝;⌜x⌝]⋅ THENA Auto) }

1
1. T : Type
2. x : bag(T)
3. #(x) = 0 ∈ ℤ
4. x ~ {}
⊢ bag-null(x) = tt

---

Latex:

---

Latex:

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


By

---

Latex:
(InstLemma  `bag-size-zero`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index