---

Step * 1 1 1 of Lemma bag-append-cancel

.....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)
BY
{ ((EqTypeD (-1) THEN Auto) THEN FLemma `cons_cancel_wrt_permutation` [-1] THEN Auto) }

---

Latex:

---

Latex:
.....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)]
\mvdash{}  (v  @  bs)  =  (v  @  cs)


By

---

Latex:
((EqTypeD  (-1)  THEN  Auto)  THEN  FLemma  `cons\_cancel\_wrt\_permutation`  [-1]  THEN  Auto)

---

Home Index