---

Step * 2 1 1 of Lemma no_repeats_iff


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)
BY
{ ((Unfold `increasing` 0 THEN Reduce 0) THEN Auto THEN (Repeat (SplitOnConclITE THEN Auto'))) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  l  :  T  List
3.  \mforall{}[x,y:T].    \mneg{}(x  =  y)  supposing  \mexists{}f:\mBbbN{}2  {}\mrightarrow{}  \mBbbN{}||l||.  (increasing(f;2)  \mwedge{}  (\mforall{}j:\mBbbN{}2.  ([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{}  increasing(\mlambda{}x.if  (x  =\msubz{}  0)  then  i  else  j  fi  ;2)


By

---

Latex:
((Unfold  `increasing`  0  THEN  Reduce  0)  THEN  Auto  THEN  (Repeat  (SplitOnConclITE  THEN  Auto')))

---

Home Index