---

Step * of Lemma equal-empty-bag

∀[T:Type]. ∀x:bag(T). ((x = {} ∈ bag(T)) ⇒ (x ~ {}))
BY
{ (Auto
   THEN (GenConcl ⌜x = L ∈ (Top List)⌝⋅ THENA Auto)
   THEN HypSubst' 3 -1
   THEN Auto
   THEN Unfold `empty-bag` -1
   THEN ThinVar `x'
   THEN ThinVar `T'
   THEN Unfold `empty-bag` 0) }

1
1. L : Top List
2. [] = L ∈ (Top List)
⊢ L ~ []

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}x:bag(T).  ((x  =  \{\})  {}\mRightarrow{}  (x  \msim{}  \{\}))


By

---

Latex:
(Auto
  THEN  (GenConcl  \mkleeneopen{}x  =  L\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  HypSubst'  3  -1
  THEN  Auto
  THEN  Unfold  `empty-bag`  -1
  THEN  ThinVar  `x'
  THEN  ThinVar  `T'
  THEN  Unfold  `empty-bag`  0)

---

Home Index