---

Step * of Lemma bag-remove1-append1

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x,y:T]. ∀[bs:bag(T)].
  (bag-remove1(eq;{y} + bs;x)
  = if eq x y then inl bs else case bag-remove1(eq;bs;x) of inl(as) => inl ({y} + as) | inr(x) => inr ⋅  fi 
  ∈ (bag(T)?))
BY
{ (Auto THEN AutoSplit) }

1
1. T : Type
2. eq : EqDecider(T)
3. x : T
4. y : T
5. ¬(x = y ∈ T)
6. bs : bag(T)
⊢ bag-remove1(eq;{y} + bs;x) = case bag-remove1(eq;bs;x) of inl(as) => inl ({y} + as) | inr(x) => inr ⋅  ∈ (bag(T)?)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[x,y:T].  \mforall{}[bs:bag(T)].
    (bag-remove1(eq;\{y\}  +  bs;x)
    =  if  eq  x  y
        then  inl  bs
        else  case  bag-remove1(eq;bs;x)  of  inl(as)  =>  inl  (\{y\}  +  as)  |  inr(x)  =>  inr  \mcdot{} 
        fi  )


By

---

Latex:
(Auto  THEN  AutoSplit)

---

Home Index