>>> inits ([] :: SList Integer) [[]] :: [[SInteger]] >>> inits [1,2,3,4::SInteger] [[],[1],[1,2],[1,2,3],[1,2,3,4]] :: [[SInteger]]
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