---

Step * of Lemma adjacent-member

∀[T:Type]. ∀L:T List. ∀x,y:T.  (adjacent(T;L;x;y) ⇒ {(x ∈ L) ∧ (y ∈ L)})
BY
{ (Auto
   THEN (((FLemma `adjacent-before` [-1]) THENM (FLemma `l_before_member`[-1]) THENM (FLemma `l_before_member2`[-2]))
         THENA Auto
         )
   ) }

1
1. [T] : Type
2. L : T List@i
3. x : T@i
4. y : T@i
5. adjacent(T;L;x;y)@i
6. x before y ∈ L
7. (y ∈ L)
8. (x ∈ L)
⊢ {(x ∈ L) ∧ (y ∈ L)}

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}L:T  List.  \mforall{}x,y:T.    (adjacent(T;L;x;y)  {}\mRightarrow{}  \{(x  \mmember{}  L)  \mwedge{}  (y  \mmember{}  L)\})


By

---

Latex:
(Auto
  THEN  (((FLemma  `adjacent-before`  [-1])
                THENM  (FLemma  `l\_before\_member`[-1])
                THENM  (FLemma  `l\_before\_member2`[-2]))
              THENA  Auto
              )
  )

---

Home Index