Step
*
2
of Lemma
bag-settype
1. T : Type
2. T List ∈ Type
3. ∀as,b1:T List. (permutation(T;as;b1) ∈ Type)
4. ∀as:T List. permutation(T;as;as)
5. a : Base
6. b : Base
7. c : a = b ∈ pertype(λas,bs. ((as ∈ T List) ∧ (bs ∈ T List) ∧ permutation(T;as;bs)))
8. a ∈ T List
9. b ∈ T List
10. permutation(T;a;b)
11. P : T ⟶ ℙ
12. ∀x:T. (x ↓∈ a
⇒ P[x])
13. a ∈ {x:T| P[x]} List
⊢ a = b ∈ bag({x:T| P[x]} )
BY
{ (InstLemma `permutation-strong-subtype` [⌜T⌝;⌜{x:T| P[x]} ⌝;⌜a⌝;⌜b⌝]⋅ THEN Auto)⋅ }
Latex:
Latex:
1. T : Type
2. T List \mmember{} Type
3. \mforall{}as,b1:T List. (permutation(T;as;b1) \mmember{} Type)
4. \mforall{}as:T List. permutation(T;as;as)
5. a : Base
6. b : Base
7. c : a = b
8. a \mmember{} T List
9. b \mmember{} T List
10. permutation(T;a;b)
11. P : T {}\mrightarrow{} \mBbbP{}
12. \mforall{}x:T. (x \mdownarrow{}\mmember{} a {}\mRightarrow{} P[x])
13. a \mmember{} \{x:T| P[x]\} List
\mvdash{} a = b
By
Latex:
(InstLemma `permutation-strong-subtype` [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}\{x:T| P[x]\} \mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{} THEN Auto)\mcdot{}
Home
Index