---

Step * 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||
⊢ Inj(ℕ||L||;ℕ||L||;λi.(||L|| - i + 1))
BY
{ (D 0 THEN Reduce 0 THEN Auto 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||
\mvdash{}  Inj(\mBbbN{}||L||;\mBbbN{}||L||;\mlambda{}i.(||L||  -  i  +  1))


By

---

Latex:
(D  0  THEN  Reduce  0  THEN  Auto  THEN  Auto')

---

Home Index