inits package:sbv

inits of a list.
>>> inits ([] :: SList Integer)
[[]] :: [[SInteger]]

>>> inits [1,2,3,4::SInteger]
[[],[1],[1,2],[1,2,3],[1,2,3,4]] :: [[SInteger]]
Construct the fully balanced initial tree, where the leaves are simply the numbers 0 through 255.
length (inits xs) == 1 + length xs
>>> runTP $ initsLength @Integer
Inductive lemma (strong): initsLength
Step: Measure is non-negative         Q.E.D.
Step: 1                               Q.E.D.
Result:                               Q.E.D.
[Proven] initsLength :: Ɐxs ∷ [Integer] → Bool