---

Step * of Lemma cons_sublist_nil

∀[T:Type]. ∀x:T. ∀L:T List.  ([x / L] ⊆ [] ⇐⇒ False)
BY
{ ((((Auto THEN FwdThruLemma `length_sublist` [(-1)]) THENA Auto) THEN Reduce (-1)) THEN Auto') }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}x:T.  \mforall{}L:T  List.    ([x  /  L]  \msubseteq{}  []  \mLeftarrow{}{}\mRightarrow{}  False)


By

---

Latex:
((((Auto  THEN  FwdThruLemma  `length\_sublist`  [(-1)])  THENA  Auto)  THEN  Reduce  (-1))  THEN  Auto')

---

Home Index