---

Step * 1 2 2 1 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)
11. i : ℕ
12. i < ||as||
⊢ as[i] = (as o f o g)[i] ∈ A
BY
{ (RWO "permute_list_select" 0 THEN Auto THEN EqCD THEN Auto)⋅ }

1
.....subterm..... T:t
1:n
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||
⊢ i = ((f o g) i) ∈ ℤ

---

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)
11.  i  :  \mBbbN{}
12.  i  <  ||as||
\mvdash{}  as[i]  =  (as  o  f  o  g)[i]


By

---

Latex:
(RWO  "permute\_list\_select"  0  THEN  Auto  THEN  EqCD  THEN  Auto)\mcdot{}

---

Home Index