---

Step * of Lemma bag-extensionality-no-repeats

No Annotations
∀[T:Type]
  ((∀x,y:T.  Dec(x = y ∈ T))
  ⇒ (∀[as,bs:bag(T)].
        uiff(as = bs ∈ bag(T);∀x:T. uiff(x ↓∈ as;x ↓∈ bs)) supposing bag-no-repeats(T;as) ∧ bag-no-repeats(T;bs)))
BY
{ (Auto THEN Try ((Unhide THEN Auto))) }

1
1. T : Type
2. ∀x,y:T.  Dec(x = y ∈ T)
3. as : bag(T)
4. bs : bag(T)
5. bag-no-repeats(T;as)
6. bag-no-repeats(T;bs)
7. ∀x:T. uiff(x ↓∈ as;x ↓∈ bs)
⊢ as = bs ∈ bag(T)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type]
    ((\mforall{}x,y:T.    Dec(x  =  y))
    {}\mRightarrow{}  (\mforall{}[as,bs:bag(T)].
                uiff(as  =  bs;\mforall{}x:T.  uiff(x  \mdownarrow{}\mmember{}  as;x  \mdownarrow{}\mmember{}  bs)) 
                supposing  bag-no-repeats(T;as)  \mwedge{}  bag-no-repeats(T;bs)))


By

---

Latex:
(Auto  THEN  Try  ((Unhide  THEN  Auto)))

---

Home Index