---

Step * of Lemma bag-lub-comm

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[as,bs:bag(T)].  (bag-lub(eq;as;bs) = bag-lub(eq;bs;as) ∈ bag(T))
BY
{ xxx(Auto THEN Unfold `bag-lub` 0 THEN RepeatFor 2 ((EqCD THEN Auto)))xxx }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[as,bs:bag(T)].    (bag-lub(eq;as;bs)  =  bag-lub(eq;bs;as))


By

---

Latex:
xxx(Auto  THEN  Unfold  `bag-lub`  0  THEN  RepeatFor  2  ((EqCD  THEN  Auto)))xxx

---

Home Index