---

Step * of Lemma no_repeats-same-length-l_contains

∀[T:Type]. ∀as,bs:T List.  (no_repeats(T;as) ⇒ (||as|| = ||bs|| ∈ ℤ) ⇒ as ⊆ bs ⇒ bs ⊆ as)
BY
{ Auto }

1
1. [T] : Type
2. as : T List
3. bs : T List
4. no_repeats(T;as)
5. ||as|| = ||bs|| ∈ ℤ
6. as ⊆ bs
⊢ bs ⊆ as

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}as,bs:T  List.    (no\_repeats(T;as)  {}\mRightarrow{}  (||as||  =  ||bs||)  {}\mRightarrow{}  as  \msubseteq{}  bs  {}\mRightarrow{}  bs  \msubseteq{}  as)


By

---

Latex:
Auto

---

Home Index