---

Step * 1 2 2 of Lemma permutation_inversion


1. A : Type
2. as : A List
3. bs : A List
4. f : ℕ||as|| ⟶ ℕ||as||
5. Inj(ℕ||as||;ℕ||as||;f)
6. bs = (as o f) ∈ (A List)
7. ||as|| = ||bs|| ∈ ℤ
8. g : ℕ||as|| ⟶ ℕ||as||
9. ∀x:ℕ||as||. ((f (g x)) = x ∈ ℤ)
10. Inj(ℕ||as||;ℕ||as||;g)
⊢ as = (as o f o g) ∈ (A List)
BY
{ (BLemma `list_extensionality` THEN Auto) }

1
1. A : Type
2. as : A List
3. bs : A List
4. f : ℕ||as|| ⟶ ℕ||as||
5. Inj(ℕ||as||;ℕ||as||;f)
6. bs = (as o f) ∈ (A List)
7. ||as|| = ||bs|| ∈ ℤ
8. g : ℕ||as|| ⟶ ℕ||as||
9. ∀x:ℕ||as||. ((f (g x)) = x ∈ ℤ)
10. Inj(ℕ||as||;ℕ||as||;g)
11. i : ℕ
12. i < ||as||
⊢ as[i] = (as o f o g)[i] ∈ A

---

Latex:

---

Latex:

1.  A  :  Type
2.  as  :  A  List
3.  bs  :  A  List
4.  f  :  \mBbbN{}||as||  {}\mrightarrow{}  \mBbbN{}||as||
5.  Inj(\mBbbN{}||as||;\mBbbN{}||as||;f)
6.  bs  =  (as  o  f)
7.  ||as||  =  ||bs||
8.  g  :  \mBbbN{}||as||  {}\mrightarrow{}  \mBbbN{}||as||
9.  \mforall{}x:\mBbbN{}||as||.  ((f  (g  x))  =  x)
10.  Inj(\mBbbN{}||as||;\mBbbN{}||as||;g)
\mvdash{}  as  =  (as  o  f  o  g)


By

---

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

---

Home Index