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