---

Step * 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 ∈ bag(B)
8. (x ∈ L)
⊢ x ∈ A
BY
{ (EqTypeD (-2) THEN Auto THEN FLemma `member-permutation` [-2] THEN Auto)⋅ }

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))
⊢ 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.  (x  \mmember{}  L)
\mvdash{}  x  \mmember{}  A


By

---

Latex:
(EqTypeD  (-2)  THEN  Auto  THEN  FLemma  `member-permutation`  [-2]  THEN  Auto)\mcdot{}

---

Home Index