---

Step * of Lemma no_repeats-merge

∀[T:Type]. ∀[bs,as:T List].  (no_repeats(T;merge(as;bs))) supposing (sorted(as) and no_repeats(T;as)) supposing T ⊆r ℤ
BY
{ (InductionOnList
   THEN Unfold `merge` 0
   THEN Reduce 0
   THEN Try (Fold `merge` 0)
   THEN Auto
   THEN BLemma `s-insert-no-repeats`
   THEN Auto
   THEN BLemma `sorted-merge`
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}[bs,as:T  List].    (no\_repeats(T;merge(as;bs)))  supposing  (sorted(as)  and  no\_repeats(T;as)) 
    supposing  T  \msubseteq{}r  \mBbbZ{}


By

---

Latex:
(InductionOnList
  THEN  Unfold  `merge`  0
  THEN  Reduce  0
  THEN  Try  (Fold  `merge`  0)
  THEN  Auto
  THEN  BLemma  `s-insert-no-repeats`
  THEN  Auto
  THEN  BLemma  `sorted-merge`
  THEN  Auto)

---

Home Index