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