---

Step * of Lemma bag-diff_wf

No Annotations
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs,as:bag(T)].  (bag-diff(eq;bs;as) ∈ bag(T)?)
BY
{ ProveWfLemma }

1
1. T : Type
2. eq : EqDecider(T)
3. bs : bag(T)
4. as : bag(T)
5. x : bag(T)
6. a : T
7. y : T
⊢ case bag-remove1(eq;x;y)
 of inl(b) =>
 bag-remove1(eq;b;a)
 | inr(z) =>
 case inl x of inl(b) => bag-remove1(eq;b;y) | inr(z) => inl x
= case case inl x of inl(b) => bag-remove1(eq;b;a) | inr(z) => inl x
   of inl(b) =>
   bag-remove1(eq;b;y)
   | inr(z) =>
   case inl x of inl(b) => bag-remove1(eq;b;a) | inr(z) => inl x
∈ (bag(T)?)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[bs,as:bag(T)].    (bag-diff(eq;bs;as)  \mmember{}  bag(T)?)


By

---

Latex:
ProveWfLemma

---

Home Index