---

Step * 1 of Lemma adjacent-reverse


1. [T] : Type
⊢ ∀x,y:T.  (adjacent(T;[];x;y) ⇐⇒ adjacent(T;[];y;x))
BY
{ ((Auto THEN FLemma `adjacent-nil` [-1]) THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
\mvdash{}  \mforall{}x,y:T.    (adjacent(T;[];x;y)  \mLeftarrow{}{}\mRightarrow{}  adjacent(T;[];y;x))


By

---

Latex:
((Auto  THEN  FLemma  `adjacent-nil`  [-1])  THEN  Auto)

---

Home Index