---

Step * 1 of Lemma l_before_no_repeats


1. T : Type
2. L : T List@i
3. i : ℕ||L||@i
4. j : ℕ||L||@i
5. no_repeats(T;L)
6. L[j] before L[i] ∈ L
7. j = i ∈ ℤ
⊢ j < i
BY
{ ((Assert ⌜False⌝⋅ THEN Auto)
   THEN (HypSubst' (-1) (-2) THENA Auto)
   THEN ThinVar `j'
   THEN RepUR ``l_before sublist`` (-1)
   THEN ExRepD
   THEN Unfold `no_repeats` (-4)
   THEN InstHyp [⌜f 0⌝;⌜f 1⌝] (-4)⋅
   THEN Auto') }

1
.....antecedent..... 
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)
⊢ ¬((f 0) = (f 1) ∈ ℕ)

2
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

---

Latex:

---

Latex:

1.  T  :  Type
2.  L  :  T  List@i
3.  i  :  \mBbbN{}||L||@i
4.  j  :  \mBbbN{}||L||@i
5.  no\_repeats(T;L)
6.  L[j]  before  L[i]  \mmember{}  L
7.  j  =  i
\mvdash{}  j  <  i


By

---

Latex:
((Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  (HypSubst'  (-1)  (-2)  THENA  Auto)
  THEN  ThinVar  `j'
  THEN  RepUR  ``l\_before  sublist``  (-1)
  THEN  ExRepD
  THEN  Unfold  `no\_repeats`  (-4)
  THEN  InstHyp  [\mkleeneopen{}f  0\mkleeneclose{};\mkleeneopen{}f  1\mkleeneclose{}]  (-4)\mcdot{}
  THEN  Auto')

---

Home Index