Step
*
of Lemma
sublist-rec-nil
∀[T:Type]. ∀[l:T List]. sublist-rec(T;[];l)
BY
{ (Auto THEN RecUnfold `sublist-rec` 0 THEN Reduce 0 THEN Auto) }
Latex:
Latex:
\mforall{}[T:Type]. \mforall{}[l:T List]. sublist-rec(T;[];l)
By
Latex:
(Auto THEN RecUnfold `sublist-rec` 0 THEN Reduce 0 THEN Auto)
Home
Index