---

Step * 3 of Lemma no_repeats_cons


1. T : Type
2. l : T List
3. x : T
4. ∀[i,j:ℕ].  (¬(l[i] = l[j] ∈ T)) supposing ((¬(i = j ∈ ℕ)) and j < ||l|| and i < ||l||)
5. ¬(x ∈ l)
6. i : ℕ
7. j : ℕ
8. i < ||l|| + 1
9. j < ||l|| + 1
10. ¬(i = j ∈ ℕ)
⊢ ¬([x / l][i] = [x / l][j] ∈ T)
BY
{ (((CaseNat 0 `i' THEN CaseNat 0 `j' THEN Reduce 0 THEN Auto THEN RWO "select_cons_tl" 0) THENA Auto)
   THEN Try ((BackThruSomeHyp THEN Auto))
   THEN Try ((ParallelOp 5 THEN Unfold `l_member` 0))
   THEN Try ((InstConcl [j - 1]⋅ THEN Complete (Auto)))
   THEN Try ((InstConcl [i - 1]⋅ THEN Complete (Auto)))) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  l  :  T  List
3.  x  :  T
4.  \mforall{}[i,j:\mBbbN{}].    (\mneg{}(l[i]  =  l[j]))  supposing  ((\mneg{}(i  =  j))  and  j  <  ||l||  and  i  <  ||l||)
5.  \mneg{}(x  \mmember{}  l)
6.  i  :  \mBbbN{}
7.  j  :  \mBbbN{}
8.  i  <  ||l||  +  1
9.  j  <  ||l||  +  1
10.  \mneg{}(i  =  j)
\mvdash{}  \mneg{}([x  /  l][i]  =  [x  /  l][j])


By

---

Latex:
(((CaseNat  0  `i'  THEN  CaseNat  0  `j'  THEN  Reduce  0  THEN  Auto  THEN  RWO  "select\_cons\_tl"  0)  THENA  Auto)
  THEN  Try  ((BackThruSomeHyp  THEN  Auto))
  THEN  Try  ((ParallelOp  5  THEN  Unfold  `l\_member`  0))
  THEN  Try  ((InstConcl  [j  -  1]\mcdot{}  THEN  Complete  (Auto)))
  THEN  Try  ((InstConcl  [i  -  1]\mcdot{}  THEN  Complete  (Auto))))

---

Home Index