---

Step * 1 2 of Lemma l_before_no_repeats


1. T : Type
2. L : T List@i
3. i : ℕ||L||@i
4. ∀[i,j:ℕ].  (¬(L[i] = L[j] ∈ T)) supposing ((¬(i = j ∈ ℕ)) and j < ||L|| and i < ||L||)
5. f : ℕ2 ⟶ ℕ||L||
6. increasing(f;2)
7. ∀j:ℕ2. ([L[i]; L[i]][j] = L[f j] ∈ T)
8. ¬(L[f 0] = L[f 1] ∈ T)
⊢ False
BY
{ (((InstHyp [⌜0⌝] (-2)⋅ THENA Auto) THEN Reduce (-1))
   THEN ((InstHyp [⌜1⌝] (-3)⋅ THENA Auto) THEN Reduce (-1))
   THEN Auto') }

---

Latex:

---

Latex:

1.  T  :  Type
2.  L  :  T  List@i
3.  i  :  \mBbbN{}||L||@i
4.  \mforall{}[i,j:\mBbbN{}].    (\mneg{}(L[i]  =  L[j]))  supposing  ((\mneg{}(i  =  j))  and  j  <  ||L||  and  i  <  ||L||)
5.  f  :  \mBbbN{}2  {}\mrightarrow{}  \mBbbN{}||L||
6.  increasing(f;2)
7.  \mforall{}j:\mBbbN{}2.  ([L[i];  L[i]][j]  =  L[f  j])
8.  \mneg{}(L[f  0]  =  L[f  1])
\mvdash{}  False


By

---

Latex:
(((InstHyp  [\mkleeneopen{}0\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)  THEN  Reduce  (-1))
  THEN  ((InstHyp  [\mkleeneopen{}1\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto)  THEN  Reduce  (-1))
  THEN  Auto')

---

Home Index