---

Step * 1 of Lemma no_repeats_safety


1. A : Type
2. tr1 : A List
3. tr2 : A List
4. tr1 ≤ tr2
5. ∀[i,j:ℕ].  (¬(tr2[i] = tr2[j] ∈ A)) supposing ((¬(i = j ∈ ℕ)) and j < ||tr2|| and i < ||tr2||)
6. i : ℕ
7. j : ℕ
8. i < ||tr1||
9. j < ||tr1||
10. ¬(i = j ∈ ℕ)
⊢ ¬(tr1[i] = tr1[j] ∈ A)
BY
{ ((((((Assert ||tr1|| ≤ ||tr2||⋅ THENL [Easy; Id]) THEN Subst tr1[i] = tr2[i] ∈ A 0⋅) THENA Auto)
     THEN Try ((BackThruLemma `iseg_select` THEN Auto))
     THEN Subst tr1[j] = tr2[j] ∈ A 0⋅)
    THENA Auto
    )
   THEN Try ((BackThruLemma `iseg_select` THEN Auto))
   THEN EasyHyp) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  tr1  :  A  List
3.  tr2  :  A  List
4.  tr1  \mleq{}  tr2
5.  \mforall{}[i,j:\mBbbN{}].    (\mneg{}(tr2[i]  =  tr2[j]))  supposing  ((\mneg{}(i  =  j))  and  j  <  ||tr2||  and  i  <  ||tr2||)
6.  i  :  \mBbbN{}
7.  j  :  \mBbbN{}
8.  i  <  ||tr1||
9.  j  <  ||tr1||
10.  \mneg{}(i  =  j)
\mvdash{}  \mneg{}(tr1[i]  =  tr1[j])


By

---

Latex:
((((((Assert  ||tr1||  \mleq{}  ||tr2||\mcdot{}  THENL  [Easy;  Id])  THEN  Subst  tr1[i]  =  tr2[i]  0\mcdot{})  THENA  Auto)
      THEN  Try  ((BackThruLemma  `iseg\_select`  THEN  Auto))
      THEN  Subst  tr1[j]  =  tr2[j]  0\mcdot{})
    THENA  Auto
    )
  THEN  Try  ((BackThruLemma  `iseg\_select`  THEN  Auto))
  THEN  EasyHyp)

---

Home Index