Step
*
of Lemma
listp_decomp
∀[T:Type]. ∀L:T List+. ∃x:T. ∃K:T List. (L = (K @ [x]) ∈ (T List))
BY
{ (Auto THEN D (-1) THEN BLemma `list_decomp_reverse` THEN Auto) }
Latex:
Latex:
\mforall{}[T:Type]. \mforall{}L:T List\msupplus{}. \mexists{}x:T. \mexists{}K:T List. (L = (K @ [x]))
By
Latex:
(Auto THEN D (-1) THEN BLemma `list\_decomp\_reverse` THEN Auto)
Home
Index