---

Step * of Lemma sub-bag-cancel-right

∀[T:Type]. ∀b1,b2,b:bag(T).  (sub-bag(T;b1 + b;b2 + b) ⇐⇒ sub-bag(T;b1;b2))
BY
{ ((UnivCD THENA Auto) THEN Unfold `sub-bag` 0 THEN D 0 THEN Auto THEN ExRepD THEN (InstConcl [⌜cs⌝]⋅ THENA Auto)) }

1
1. T : Type
2. b1 : bag(T)
3. b2 : bag(T)
4. b : bag(T)
5. cs : bag(T)
6. (b2 + b) = ((b1 + b) + cs) ∈ bag(T)
⊢ b2 = (b1 + cs) ∈ bag(T)

2
1. T : Type
2. b1 : bag(T)
3. b2 : bag(T)
4. b : bag(T)
5. cs : bag(T)
6. b2 = (b1 + cs) ∈ bag(T)
⊢ (b2 + b) = ((b1 + b) + cs) ∈ bag(T)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}b1,b2,b:bag(T).    (sub-bag(T;b1  +  b;b2  +  b)  \mLeftarrow{}{}\mRightarrow{}  sub-bag(T;b1;b2))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `sub-bag`  0
  THEN  D  0
  THEN  Auto
  THEN  ExRepD
  THEN  (InstConcl  [\mkleeneopen{}cs\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index