---

Step * of Lemma bag-append-ident

∀[T:Type]. ∀[as:bag(T)].  (((as + {}) = as ∈ bag(T)) ∧ (({} + as) = as ∈ bag(T)))
BY
{ (((Auto THEN Reduce 0) THEN Auto) THEN RWO "bag-append-empty" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[as:bag(T)].    (((as  +  \{\})  =  as)  \mwedge{}  ((\{\}  +  as)  =  as))


By

---

Latex:
(((Auto  THEN  Reduce  0)  THEN  Auto)  THEN  RWO  "bag-append-empty"  0  THEN  Auto)

---

Home Index