---

Step * of Lemma es-interface-predecessors-no_repeats2

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(Top)]. ∀[e:E].  no_repeats({a:E(X)| loc(a) = loc(e) ∈ Id} ;≤(X)(e))
BY
{ (InstLemma `es-interface-predecessors-no_repeats` [] THEN RepeatFor 10 ((ParallelLast' THENA Auto))) }

1
1. Info : Type
2. es : EO+(Info)
3. X : EClass(Top)
4. e : E
5. i : ℕ
6. j : ℕ
7. i < ||≤(X)(e)||
8. j < ||≤(X)(e)||
9. ¬(i = j ∈ ℕ)
10. ¬(≤(X)(e)[i] = ≤(X)(e)[j] ∈ E(X))
⊢ ¬(≤(X)(e)[i] = ≤(X)(e)[j] ∈ {a:E(X)| loc(a) = loc(e) ∈ Id} )

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X:EClass(Top)].  \mforall{}[e:E].    no\_repeats(\{a:E(X)|  loc(a)  =  loc(e)\}  ;\mleq{}(X)\000C(e))


By

---

Latex:
(InstLemma  `es-interface-predecessors-no\_repeats`  []  THEN  RepeatFor  10  ((ParallelLast'  THENA  Auto)))

---

Home Index