---

Step * 1 of Lemma permutation-sv-list


1. A : Type
2. L1 : A List
3. L2 : A List
4. single-valued-list(L1;A)@i
5. permutation(A;L1;L2)@i
⊢ L1 = L2 ∈ (A List)
BY
{ (BLemma `list_extensionality` THEN Auto) }

1
1. A : Type
2. L1 : A List
3. L2 : A List
4. single-valued-list(L1;A)@i
5. permutation(A;L1;L2)@i
⊢ ||L1|| = ||L2|| ∈ ℤ

2
1. A : Type
2. L1 : A List
3. L2 : A List
4. single-valued-list(L1;A)@i
5. permutation(A;L1;L2)@i
6. i : ℕ@i
7. i < ||L1||@i
⊢ L1[i] = L2[i] ∈ A

---

Latex:

---

Latex:

1.  A  :  Type
2.  L1  :  A  List
3.  L2  :  A  List
4.  single-valued-list(L1;A)@i
5.  permutation(A;L1;L2)@i
\mvdash{}  L1  =  L2


By

---

Latex:
(BLemma  `list\_extensionality`  THEN  Auto)

---

Home Index