---

Step * 1 1 1 of Lemma bag-member-strong-subtype


1. A : Type
2. B : Type
3. strong-subtype(A;B)
4. b : A List
5. x : B
6. L : B List
7. L = b ∈ pertype(λas,bs. ((as ∈ B List) ∧ (bs ∈ B List) ∧ permutation(B;as;bs)))
8. L ∈ B List
9. b ∈ B List
10. permutation(B;L;b)
11. (x ∈ L)
12. ∀a:B. ((a ∈ L) ⇐⇒ (a ∈ b))
13. (x ∈ L) ⇐ (x ∈ b)
14. (x ∈ b)
⊢ x ∈ A
BY
{ RepeatFor 2 (D (-1)) }

1
1. A : Type
2. B : Type
3. strong-subtype(A;B)
4. b : A List
5. x : B
6. L : B List
7. L = b ∈ pertype(λas,bs. ((as ∈ B List) ∧ (bs ∈ B List) ∧ permutation(B;as;bs)))
8. L ∈ B List
9. b ∈ B List
10. permutation(B;L;b)
11. (x ∈ L)
12. ∀a:B. ((a ∈ L) ⇐⇒ (a ∈ b))
13. (x ∈ L) ⇐ (x ∈ b)
14. i : ℕ
15. i < ||b||
16. x = b[i] ∈ B
⊢ x ∈ A

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  strong-subtype(A;B)
4.  b  :  A  List
5.  x  :  B
6.  L  :  B  List
7.  L  =  b
8.  L  \mmember{}  B  List
9.  b  \mmember{}  B  List
10.  permutation(B;L;b)
11.  (x  \mmember{}  L)
12.  \mforall{}a:B.  ((a  \mmember{}  L)  \mLeftarrow{}{}\mRightarrow{}  (a  \mmember{}  b))
13.  (x  \mmember{}  L)  \mLeftarrow{}{}  (x  \mmember{}  b)
14.  (x  \mmember{}  b)
\mvdash{}  x  \mmember{}  A


By

---

Latex:
RepeatFor  2  (D  (-1))

---

Home Index