---

Step * of Lemma merge-int-one-one

∀[T:Type]
  ∀[as,bs,cs:T List].
    (as = bs ∈ (T List)) supposing 
       ((merge-int(cs;as) = merge-int(cs;bs) ∈ (T List)) and 
       sorted(bs) and 
       sorted(as) and 
       sorted(cs)) 
  supposing T ⊆r ℤ
BY
{ (Auto THEN (RWO "merge-int-comm" (-1) THENA Auto) THEN FLemma `merge-int-1-1` [-1] THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  (RWO  "merge-int-comm"  (-1)  THENA  Auto)  THEN  FLemma  `merge-int-1-1`  [-1]  THEN  Auto)

---

Home Index