---

Step * 1 2 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))
⊢ rev(L) = (L o λi.(||L|| - i + 1)) ∈ (A List)
BY
{ (BLemma `list_extensionality`⋅ THEN Auto) }

1
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)||
⊢ rev(L)[i] = (L o λi.(||L|| - i + 1))[i] ∈ A

---

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))
\mvdash{}  rev(L)  =  (L  o  \mlambda{}i.(||L||  -  i  +  1))


By

---

Latex:
(BLemma  `list\_extensionality`\mcdot{}  THEN  Auto)

---

Home Index