---

Step * of Lemma merge-strict-exists

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  (Trans(T;a,b.R a b)
  ⇒ (∀sa,sb:T List.
        ((∀a,b:T.  ((a ∈ sa) ⇒ (b ∈ sb) ⇒ ((R a b) ∨ (R b a))))
        ⇒ sorted-by(R;sa)
        ⇒ sorted-by(R;sb)
        ⇒ (∃sc:T List. (sorted-by(R;sc) ∧ sa ⊆ sc ∧ sb ⊆ sc ∧ sc ⊆ sa @ sb)))))
BY
{ (RepeatFor 3 ((D 0 THENA Auto))
   THEN InductionOnList
   THEN Try ((Auto
              THEN Reduce 0
              THEN With ⌜sb⌝ (D 0)⋅
              THEN Auto
              THEN Try ((BLemma `l_contains_nil` THEN Auto))
              THEN BLemma `l_contains_weakening`
              THEN Complete (Auto)))) }

1
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. Trans(T;a,b.R a b)
4. u : T
5. v : T List
6. ∀sb:T List
     ((∀a,b:T.  ((a ∈ v) ⇒ (b ∈ sb) ⇒ ((R a b) ∨ (R b a))))
     ⇒ sorted-by(R;v)
     ⇒ sorted-by(R;sb)
     ⇒ (∃sc:T List. (sorted-by(R;sc) ∧ v ⊆ sc ∧ sb ⊆ sc ∧ sc ⊆ v @ sb)))
⊢ ∀sb:T List
    ((∀a,b:T.  ((a ∈ [u / v]) ⇒ (b ∈ sb) ⇒ ((R a b) ∨ (R b a))))
    ⇒ sorted-by(R;[u / v])
    ⇒ sorted-by(R;sb)
    ⇒ (∃sc:T List. (sorted-by(R;sc) ∧ [u / v] ⊆ sc ∧ sb ⊆ sc ∧ sc ⊆ [u / v] @ sb)))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    (Trans(T;a,b.R  a  b)
    {}\mRightarrow{}  (\mforall{}sa,sb:T  List.
                ((\mforall{}a,b:T.    ((a  \mmember{}  sa)  {}\mRightarrow{}  (b  \mmember{}  sb)  {}\mRightarrow{}  ((R  a  b)  \mvee{}  (R  b  a))))
                {}\mRightarrow{}  sorted-by(R;sa)
                {}\mRightarrow{}  sorted-by(R;sb)
                {}\mRightarrow{}  (\mexists{}sc:T  List.  (sorted-by(R;sc)  \mwedge{}  sa  \msubseteq{}  sc  \mwedge{}  sb  \msubseteq{}  sc  \mwedge{}  sc  \msubseteq{}  sa  @  sb)))))


By

---

Latex:
(RepeatFor  3  ((D  0  THENA  Auto))
  THEN  InductionOnList
  THEN  Try  ((Auto
                        THEN  Reduce  0
                        THEN  With  \mkleeneopen{}sb\mkleeneclose{}  (D  0)\mcdot{}
                        THEN  Auto
                        THEN  Try  ((BLemma  `l\_contains\_nil`  THEN  Auto))
                        THEN  BLemma  `l\_contains\_weakening`
                        THEN  Complete  (Auto))))

---

Home Index