---

Step * 1 2 1 1 1 1 1 1 1 of Lemma empty-bag-union


1. T : Type
2. u : bag(T)
3. v : bag(T) List
4. u = {} ∈ bag(T)
5. reduce(λl,l'. (l + l');{};v) = {} ∈ bag(T)
6. x : Top List
7. x = u ∈ (Top List)
8. ∀x:Top List. ((x ∈ v) ⇒ (x ~ {}))
⊢ x ~ {}
BY
{ (FLemma `equal-empty-bag` [-5] THEN Auto)⋅ }

1
1. T : Type
2. u : bag(T)
3. v : bag(T) List
4. u = {} ∈ bag(T)
5. reduce(λl,l'. (l + l');{};v) = {} ∈ bag(T)
6. x : Top List
7. x = u ∈ (Top List)
8. ∀x:Top List. ((x ∈ v) ⇒ (x ~ {}))
9. u ~ {}
⊢ x ~ {}

---

Latex:

---

Latex:

1.  T  :  Type
2.  u  :  bag(T)
3.  v  :  bag(T)  List
4.  u  =  \{\}
5.  reduce(\mlambda{}l,l'.  (l  +  l');\{\};v)  =  \{\}
6.  x  :  Top  List
7.  x  =  u
8.  \mforall{}x:Top  List.  ((x  \mmember{}  v)  {}\mRightarrow{}  (x  \msim{}  \{\}))
\mvdash{}  x  \msim{}  \{\}


By

---

Latex:
(FLemma  `equal-empty-bag`  [-5]  THEN  Auto)\mcdot{}

---

Home Index