---

Step * 1 1 of Lemma class-output-support-no_repeats


1. Info : Type
2. T : Type
3. es : EO+(Info)
4. L : E List
5. no_repeats(E;L)
6. ∀e1,e2:E.  (e2 ↓∈ L ⇒ e1 ↓∈ L ⇒ (¬(e1 <loc e2)))
⊢ no_repeats(E;concat(map(λe.≤loc(e);L)))
BY
{ (BLemma `no_repeats_concat`
   THEN Auto
   THEN ((All (RWW "length-map-sq") THEN Auto) THEN ((RWW "select-map" 0⋅ THENM Reduce 0) THEN Auto)⋅)⋅) }

1
1. Info : Type
2. T : Type
3. es : EO+(Info)
4. L : E List
5. no_repeats(E;L)
6. ∀e1,e2:E.  (e2 ↓∈ L ⇒ e1 ↓∈ L ⇒ (¬(e1 <loc e2)))
7. i : ℕ||L||@i
8. no_repeats(E;map(λe.≤loc(e);L)[i])
9. j : {j:ℕ||L||| ¬(i = j ∈ ℤ)} @i
10. k : ℕ||map(λe.≤loc(e);L)[i]||@i
⊢ ¬(≤loc(L[i])[k] ∈ ≤loc(L[j]))

---

Latex:



1.  Info  :  Type
2.  T  :  Type
3.  es  :  EO+(Info)
4.  L  :  E  List
5.  no\_repeats(E;L)
6.  \mforall{}e1,e2:E.    (e2  \mdownarrow{}\mmember{}  L  {}\mRightarrow{}  e1  \mdownarrow{}\mmember{}  L  {}\mRightarrow{}  (\mneg{}(e1  <loc  e2)))
\mvdash{}  no\_repeats(E;concat(map(\mlambda{}e.\mleq{}loc(e);L)))


By

(BLemma  `no\_repeats\_concat`
  THEN  Auto
  THEN  ((All  (RWW  "length-map-sq")  THEN  Auto)  THEN  ((RWW  "select-map"  0\mcdot{}  THENM  Reduce  0)  THEN  Auto)\mcdot{})
  \mcdot{})

---

Home Index