---

Step * of Lemma adjacent-to-same-sublist2

∀[T:Type]
  ∀L1,L2:T List. ∀a,b,c:T.
    L1 ⊆ L2 ⇒ adjacent(T;L1;a;b) ⇒ adjacent(T;L2;a;c) ⇒ (c before b ∈ L2 ∨ (b = c ∈ T)) supposing no_repeats(T;L2)
BY
{ (Auto THEN ((FLemma `adjacent-sublist` [-3; -2]) THENM (FLemma `before-adjacent2` [-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;a;b)  {}\mRightarrow{}  adjacent(T;L2;a;c)  {}\mRightarrow{}  (c  before  b  \mmember{}  L2  \mvee{}  (b  =  c)) 
        supposing  no\_repeats(T;L2)


By

---

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

---

Home Index