---

Step * 1 of Lemma no_repeats-sublist


1. T : Type
2. L : T List
3. L' : T List
4. ∀[x,y:T].  ¬(x = y ∈ T) supposing x before y ∈ L
5. L' ⊆ L
6. x : T
7. y : T
8. x before y ∈ L'
⊢ ¬(x = y ∈ T)
BY
{ TACTIC:(FLemma `l_before_sublist` [5] THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  L  :  T  List
3.  L'  :  T  List
4.  \mforall{}[x,y:T].    \mneg{}(x  =  y)  supposing  x  before  y  \mmember{}  L
5.  L'  \msubseteq{}  L
6.  x  :  T
7.  y  :  T
8.  x  before  y  \mmember{}  L'
\mvdash{}  \mneg{}(x  =  y)


By

---

Latex:
TACTIC:(FLemma  `l\_before\_sublist`  [5]  THEN  Auto)

---

Home Index