---

Step * 1 2 1 1 of Lemma permutation-sv-list


1. A : Type
2. L1 : A List
3. L2 : A List
4. single-valued-list(L1;A)@i
5. f : ℕ||L1|| ─→ ℕ||L1||@i
6. Inj(ℕ||L1||;ℕ||L1||;f)@i
7. L2 = (L1 o f) ∈ (A List)@i
8. i : ℕ@i
9. i < ||L1||@i
10. 0 ≤ i
⊢ i < ||L2||
BY
{ HypSubst' 7 0 }

1
1. A : Type
2. L1 : A List
3. L2 : A List
4. single-valued-list(L1;A)@i
5. f : ℕ||L1|| ─→ ℕ||L1||@i
6. Inj(ℕ||L1||;ℕ||L1||;f)@i
7. L2 = (L1 o f) ∈ (A List)@i
8. i : ℕ@i
9. i < ||L1||@i
10. 0 ≤ i
⊢ i < ||(L1 o f)||

---

Latex:

---

Latex:

1.  A  :  Type
2.  L1  :  A  List
3.  L2  :  A  List
4.  single-valued-list(L1;A)@i
5.  f  :  \mBbbN{}||L1||  {}\mrightarrow{}  \mBbbN{}||L1||@i
6.  Inj(\mBbbN{}||L1||;\mBbbN{}||L1||;f)@i
7.  L2  =  (L1  o  f)@i
8.  i  :  \mBbbN{}@i
9.  i  <  ||L1||@i
10.  0  \mleq{}  i
\mvdash{}  i  <  ||L2||


By

---

Latex:
HypSubst'  7  0

---

Home Index