---

Step * of Lemma bag-void-sq-empty

∀[T:Type]. ∀x:bag(T). x ~ {} supposing ¬T
BY
{ (Auto
   THEN BLemma `equal-empty-bag`
   THEN Auto
   THEN DVar `x'
   THEN (Subst' x ~ {} 0 THENM Auto)
   THEN (GenConcl ⌜x = L ∈ (T List)⌝⋅ THENA Auto)
   THEN Thin (-1)
   THEN D -1
   THEN Auto
   THEN Computation) }

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  BLemma  `equal-empty-bag`
  THEN  Auto
  THEN  DVar  `x'
  THEN  (Subst'  x  \msim{}  \{\}  0  THENM  Auto)
  THEN  (GenConcl  \mkleeneopen{}x  =  L\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  D  -1
  THEN  Auto
  THEN  Computation)

---

Home Index