---

Step * 1 1 of Lemma bag-append-cancel


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)
BY
{ (Reduce (-1) THEN D -2 THEN Auto) }

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

---

Latex:

---

Latex:

1.  T  :  Type
2.  bs  :  T  List
3.  cs  :  T  List
4.  u  :  T
5.  v  :  T  List
6.  ((v  @  bs)  =  (v  @  cs))  {}\mRightarrow{}  (bs  =  cs)
7.  ([u  /  v]  @  bs)  =  ([u  /  v]  @  cs)
\mvdash{}  bs  =  cs


By

---

Latex:
(Reduce  (-1)  THEN  D  -2  THEN  Auto)

---

Home Index