---

Step * of Lemma subtype-bag-only

∀[T:Type]. ∀[bs:bag(T)].  bs ∈ bag({x:T| x = only(bs) ∈ T} ) supposing #(bs) = 1 ∈ ℤ
BY
{ ((UnivCD ⋅ THENA Auto)
   THEN (InstLemma `bag-size-one` [⌜T⌝;⌜bs⌝]⋅ THENA Auto)
   THEN RW (AddrC [2] (HypC (-1))) 0
   THEN (GenConclTerm ⌜only(bs)⌝⋅ THENA Auto)
   THEN All Thin) }

1
1. T : Type
2. v : T
⊢ {v} ∈ bag({x:T| x = v ∈ T} )

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[bs:bag(T)].    bs  \mmember{}  bag(\{x:T|  x  =  only(bs)\}  )  supposing  \#(bs)  =  1


By

---

Latex:
((UnivCD  \mcdot{}  THENA  Auto)
  THEN  (InstLemma  `bag-size-one`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}bs\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RW  (AddrC  [2]  (HypC  (-1)))  0
  THEN  (GenConclTerm  \mkleeneopen{}only(bs)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Thin)

---

Home Index