---

Step * of Lemma compat-iseg2

∀[T:Type]. ∀L1,L2,L3:T List.  (L1 ≤ L2 ⇒ L3 || L2 ⇒ L3 || L1)
BY
{ (Auto
   THEN BLemma `compat_symmetry`
   THEN Auto
   THEN (Using [`L2',⌜L2⌝] (BLemma `compat-iseg`))⋅
   THEN Auto
   THEN BLemma `compat_symmetry`
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}L1,L2,L3:T  List.    (L1  \mleq{}  L2  {}\mRightarrow{}  L3  ||  L2  {}\mRightarrow{}  L3  ||  L1)


By

---

Latex:
(Auto
  THEN  BLemma  `compat\_symmetry`
  THEN  Auto
  THEN  (Using  [`L2',\mkleeneopen{}L2\mkleeneclose{}]  (BLemma  `compat-iseg`))\mcdot{}
  THEN  Auto
  THEN  BLemma  `compat\_symmetry`
  THEN  Auto)

---

Home Index