Step
*
of Lemma
firstn_append_front_singleton
∀[L:Top List]. ∀a:Top. (firstn(||L @ [a]|| - 1;L @ [a]) ~ L)
BY
{ (Auto THEN Subst 1 ~ ||[a]|| 0⋅ THEN Auto) }
Latex:
Latex:
\mforall{}[L:Top List]. \mforall{}a:Top. (firstn(||L @ [a]|| - 1;L @ [a]) \msim{} L)
By
Latex:
(Auto THEN Subst 1 \msim{} ||[a]|| 0\mcdot{} THEN Auto)
Home
Index