---

Step * 2 of Lemma no_repeats-permute


1. ∀T:Type. ∀as,bs:T List.  (no_repeats(T;as @ bs) ⇒ no_repeats(T;bs @ as))
⊢ ∀[T:Type]. ∀[as,bs:T List].  uiff(no_repeats(T;as @ bs);no_repeats(T;bs @ as))
BY
{ Auto }

---

Latex:

---

Latex:

1.  \mforall{}T:Type.  \mforall{}as,bs:T  List.    (no\_repeats(T;as  @  bs)  {}\mRightarrow{}  no\_repeats(T;bs  @  as))
\mvdash{}  \mforall{}[T:Type].  \mforall{}[as,bs:T  List].    uiff(no\_repeats(T;as  @  bs);no\_repeats(T;bs  @  as))


By

---

Latex:
Auto

---

Home Index