---

Step * 2 1 of Lemma no_repeats_iff


1. T : Type
2. l : T List
3. ∀[x,y:T].
     ¬(x = y ∈ T) 
     supposing ∃f:ℕ||[x; y]|| ⟶ ℕ||l||. (increasing(f;||[x; y]||) ∧ (∀j:ℕ||[x; y]||. ([x; y][j] = l[f j] ∈ T)))
4. i : ℕ
5. j : ℕ
6. i < ||l||
7. j < ||l||
8. ¬(i = j ∈ ℕ)
9. i < j
⊢ ¬(l[i] = l[j] ∈ T)
BY
{ ((((((BackThruSomeHyp THEN Auto) THEN InstConcl [λx.if (x =z 0) then i else j fi ]) THEN Reduce 0) THEN Auto)
    THEN All Reduce
    )
   THEN Auto
   ) }

1
1. T : Type
2. l : T List
3. ∀[x,y:T].  ¬(x = y ∈ T) supposing ∃f:ℕ2 ⟶ ℕ||l||. (increasing(f;2) ∧ (∀j:ℕ2. ([x; y][j] = l[f j] ∈ T)))
4. i : ℕ
5. j : ℕ
6. i < ||l||
7. j < ||l||
8. ¬(i = j ∈ ℕ)
9. i < j
⊢ increasing(λx.if (x =z 0) then i else j fi ;2)

2
1. T : Type
2. l : T List
3. ∀[x,y:T].  ¬(x = y ∈ T) supposing ∃f:ℕ2 ⟶ ℕ||l||. (increasing(f;2) ∧ (∀j:ℕ2. ([x; y][j] = l[f j] ∈ T)))
4. i : ℕ
5. j : ℕ
6. i < ||l||
7. j < ||l||
8. ¬(i = j ∈ ℕ)
9. i < j
10. increasing(λx.if (x =z 0) then i else j fi ;2)
11. j1 : ℕ2
⊢ [l[i]; l[j]][j1] = l[if (j1 =z 0) then i else j fi ] ∈ T

---

Latex:

---

Latex:

1.  T  :  Type
2.  l  :  T  List
3.  \mforall{}[x,y:T].
          \mneg{}(x  =  y) 
          supposing  \mexists{}f:\mBbbN{}||[x;  y]||  {}\mrightarrow{}  \mBbbN{}||l||
                                (increasing(f;||[x;  y]||)  \mwedge{}  (\mforall{}j:\mBbbN{}||[x;  y]||.  ([x;  y][j]  =  l[f  j])))
4.  i  :  \mBbbN{}
5.  j  :  \mBbbN{}
6.  i  <  ||l||
7.  j  <  ||l||
8.  \mneg{}(i  =  j)
9.  i  <  j
\mvdash{}  \mneg{}(l[i]  =  l[j])


By

---

Latex:
((((((BackThruSomeHyp  THEN  Auto)  THEN  InstConcl  [\mlambda{}x.if  (x  =\msubz{}  0)  then  i  else  j  fi  ])  THEN  Reduce  0)
      THEN  Auto
      )
    THEN  All  Reduce
    )
  THEN  Auto
  )

---

Home Index