---

Step * of Lemma bag-bind-empty-right

∀A:Type. ∀ba:bag(A).  (bag-bind(ba;λa.{}) ~ {})
BY
{ (Auto THEN (GenConcl ⌜ba = L ∈ (Top List)⌝⋅ THENA Auto)) }

1
1. A : Type
2. ba : bag(A)
3. L : Top List
4. ba = L ∈ (Top List)
⊢ bag-bind(L;λa.{}) ~ {}

---

Latex:

---

Latex:
\mforall{}A:Type.  \mforall{}ba:bag(A).    (bag-bind(ba;\mlambda{}a.\{\})  \msim{}  \{\})


By

---

Latex:
(Auto  THEN  (GenConcl  \mkleeneopen{}ba  =  L\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index