---

Step * of Lemma no_repeats-subtype

∀[T,S:Type].  ∀[L:S List]. no_repeats(S;L) supposing no_repeats(T;L) supposing S ⊆r T
BY
{ (Auto THEN RepeatFor 8 (ParallelLast)) }

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  RepeatFor  8  (ParallelLast))

---

Home Index