---

Step * of Lemma no_repeats-permute

∀[T:Type]. ∀[as,bs:T List].  uiff(no_repeats(T;as @ bs);no_repeats(T;bs @ as))
BY
{ xxxAssert ⌜∀T:Type. ∀as,bs:T List.  (no_repeats(T;as @ bs) ⇒ no_repeats(T;bs @ as))⌝⋅xxx }

1
.....assertion..... 
∀T:Type. ∀as,bs:T List.  (no_repeats(T;as @ bs) ⇒ no_repeats(T;bs @ as))

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

---

Latex:

---

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


By

---

Latex:
xxxAssert  \mkleeneopen{}\mforall{}T:Type.  \mforall{}as,bs:T  List.    (no\_repeats(T;as  @  bs)  {}\mRightarrow{}  no\_repeats(T;bs  @  as))\mkleeneclose{}\mcdot{}xxx

---

Home Index