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