---

Step * of Lemma bag-extensionality1

∀[T:Type]. ∀[eq:T ⟶ T ⟶ 𝔹].
  ∀[as,bs:bag(T)].  uiff(as = bs ∈ bag(T);∀x:T. (#([y∈as|eq x y]) = #([y∈bs|eq x y]) ∈ ℤ)) 
  supposing ∀[x,y:T].  (↑(eq x y) ⇐⇒ x = y ∈ T)
BY
{ (Auto THEN Try (RepeatFor 2 ((EqCD THEN Auto))⋅)) }

1
1. T : Type
2. eq : T ⟶ T ⟶ 𝔹
3. ∀[x,y:T].  (↑(eq x y) ⇐⇒ x = y ∈ T)
4. as : bag(T)
5. bs : bag(T)
6. ∀x:T. (#([y∈as|eq x y]) = #([y∈bs|eq x y]) ∈ ℤ)
⊢ as = bs ∈ bag(T)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}].
    \mforall{}[as,bs:bag(T)].    uiff(as  =  bs;\mforall{}x:T.  (\#([y\mmember{}as|eq  x  y])  =  \#([y\mmember{}bs|eq  x  y]))) 
    supposing  \mforall{}[x,y:T].    (\muparrow{}(eq  x  y)  \mLeftarrow{}{}\mRightarrow{}  x  =  y)


By

---

Latex:
(Auto  THEN  Try  (RepeatFor  2  ((EqCD  THEN  Auto))\mcdot{}))

---

Home Index