---

Step * of Lemma no_repeats-sublist

∀[T:Type]. ∀[L,L':T List].  (no_repeats(T;L')) supposing (L' ⊆ L and no_repeats(T;L))
BY
{ (RepeatFor 3 (Intro) THEN RWO "no_repeats_iff" 0 THEN Auto) }

1
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)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L,L':T  List].    (no\_repeats(T;L'))  supposing  (L'  \msubseteq{}  L  and  no\_repeats(T;L))


By

---

Latex:
(RepeatFor  3  (Intro)  THEN  RWO  "no\_repeats\_iff"  0  THEN  Auto)

---

Home Index