---

Step * 1 of Lemma bag-append-cancel


1. T : Type
2. as : T List
3. bs : T List
4. cs : T List
5. (as + bs) = (as + cs) ∈ bag(T)
⊢ bs = cs ∈ bag(T)
BY
{ (Unfold `bag-append` -1 THEN ListInd 2 THEN Auto) }

1
1. T : Type
2. bs : T List
3. cs : T List
4. u : T
5. v : T List
6. ((v @ bs) = (v @ cs) ∈ bag(T)) ⇒ (bs = cs ∈ bag(T))
7. ([u / v] @ bs) = ([u / v] @ cs) ∈ bag(T)
⊢ bs = cs ∈ bag(T)

---

Latex:

---

Latex:

1.  T  :  Type
2.  as  :  T  List
3.  bs  :  T  List
4.  cs  :  T  List
5.  (as  +  bs)  =  (as  +  cs)
\mvdash{}  bs  =  cs


By

---

Latex:
(Unfold  `bag-append`  -1  THEN  ListInd  2  THEN  Auto)

---

Home Index