---

Step * of Lemma adjacent-to-same-sublist

∀[T:Type]
  ∀L1,L2:T List. ∀a,b,c:T.
    L1 ⊆ L2 ⇒ adjacent(T;L1;b;a) ⇒ adjacent(T;L2;c;a) ⇒ (b before c ∈ L2 ∨ (b = c ∈ T)) supposing no_repeats(T;L2)
BY
{ (Auto THEN ((FLemma `adjacent-sublist` [-3; -2]) THENM (FLemma `before-adjacent` [-2; -1])) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}L1,L2:T  List.  \mforall{}a,b,c:T.
        L1  \msubseteq{}  L2  {}\mRightarrow{}  adjacent(T;L1;b;a)  {}\mRightarrow{}  adjacent(T;L2;c;a)  {}\mRightarrow{}  (b  before  c  \mmember{}  L2  \mvee{}  (b  =  c)) 
        supposing  no\_repeats(T;L2)


By

---

Latex:
(Auto
  THEN  ((FLemma  `adjacent-sublist`  [-3;  -2])  THENM  (FLemma  `before-adjacent`  [-2;  -1]))
  THEN  Auto)

---

Home Index