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