---

Step * 1 2 1 1 of Lemma permutation-reverse


1. A : Type
2. L : A List
3. λi.(||L|| - i + 1) ∈ ℕ||L|| ⟶ ℕ||L||
4. ||rev(L)|| ~ ||L||
5. ||(L o λi.(||L|| - i + 1))|| ~ ||L||
6. Inj(ℕ||L||;ℕ||L||;λi.(||L|| - i + 1))
7. i : ℕ
8. i < ||rev(L)||
9. i < ||L||
⊢ rev(L)[i] = (L o λi.(||L|| - i + 1))[i] ∈ A
BY
{ (RWO "select-reverse permute_list_select" 0 THEN Reduce 0 THEN Auto')⋅ }

---

Latex:

---

Latex:

1.  A  :  Type
2.  L  :  A  List
3.  \mlambda{}i.(||L||  -  i  +  1)  \mmember{}  \mBbbN{}||L||  {}\mrightarrow{}  \mBbbN{}||L||
4.  ||rev(L)||  \msim{}  ||L||
5.  ||(L  o  \mlambda{}i.(||L||  -  i  +  1))||  \msim{}  ||L||
6.  Inj(\mBbbN{}||L||;\mBbbN{}||L||;\mlambda{}i.(||L||  -  i  +  1))
7.  i  :  \mBbbN{}
8.  i  <  ||rev(L)||
9.  i  <  ||L||
\mvdash{}  rev(L)[i]  =  (L  o  \mlambda{}i.(||L||  -  i  +  1))[i]


By

---

Latex:
(RWO  "select-reverse  permute\_list\_select"  0  THEN  Reduce  0  THEN  Auto')\mcdot{}

---

Home Index