---

Step * of Lemma bag-drop-head

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs:bag(T)]. ∀[x:T].  (bag-drop(eq;[x / bs];x) ~ bs)
BY
{ xxx(Auto THEN (RepUR ``bag-drop`` 0 THEN Subst' bag-remove1(eq;[x / bs];x) ~ inl bs 0 THEN Reduce 0 THEN Auto)⋅)xxx }

1
.....equality..... 
1. T : Type
2. eq : EqDecider(T)
3. bs : bag(T)
4. x : T
⊢ bag-remove1(eq;[x / bs];x) ~ inl bs

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[bs:bag(T)].  \mforall{}[x:T].    (bag-drop(eq;[x  /  bs];x)  \msim{}  bs)


By

---

Latex:
xxx(Auto
        THEN  (RepUR  ``bag-drop``  0
                    THEN  Subst'  bag-remove1(eq;[x  /  bs];x)  \msim{}  inl  bs  0
                    THEN  Reduce  0
                    THEN  Auto)\mcdot{}
        )xxx

---

Home Index