---

Step * of Lemma bag-append-eq-empty

∀[T:Type]. ∀[b1,b2:bag(T)].  uiff((b1 + b2) = {} ∈ bag(T);(b1 = {} ∈ bag(T)) ∧ (b2 = {} ∈ bag(T)))
BY
{ ((UnivCD THENA Auto) THEN RepeatFor 2 ((D 0 THENA Auto))) }

1
1. T : Type
2. b1 : bag(T)
3. b2 : bag(T)
4. (b1 + b2) = {} ∈ bag(T)
⊢ (b1 = {} ∈ bag(T)) ∧ (b2 = {} ∈ bag(T))

2
1. T : Type
2. b1 : bag(T)
3. b2 : bag(T)
4. (b1 = {} ∈ bag(T)) ∧ (b2 = {} ∈ bag(T))
⊢ (b1 + b2) = {} ∈ bag(T)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[b1,b2:bag(T)].    uiff((b1  +  b2)  =  \{\};(b1  =  \{\})  \mwedge{}  (b2  =  \{\}))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  RepeatFor  2  ((D  0  THENA  Auto)))

---

Home Index