---

Step * of Lemma unshuffle-iseg

∀[T:Type]. ∀as,bs:T List.  (as ≤ bs ⇒ unshuffle(as) ≤ unshuffle(bs))
BY
{ (InductionOnLength THEN Auto) }

1
1. [T] : Type
2. n : ℕ
3. as : T List
4. ∀a1:T List. (||a1|| < ||as|| ⇒ (∀bs:T List. (a1 ≤ bs ⇒ unshuffle(a1) ≤ unshuffle(bs))))
5. bs : T List
6. as ≤ bs
⊢ unshuffle(as) ≤ unshuffle(bs)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}as,bs:T  List.    (as  \mleq{}  bs  {}\mRightarrow{}  unshuffle(as)  \mleq{}  unshuffle(bs))


By

---

Latex:
(InductionOnLength  THEN  Auto)

---

Home Index