Does Welder have a concept of strong induction?

Other Questions Notion
1

In Welder, strong induction seems unavailable for proving that folds remain equal after element removal. For example:

def aggregate(items, init, combiner):
    if not items:
        return init
    return combiner(items[0], aggregate(items[1:], init, combiner))
2

In my work with Welder, I haven’t seen a built-in framework for strong induction either. I typically rely on the program’s recursive structure and a traditional form of induction to prove properties such as the equality of folds after element removal. Occasionally, I augment my proofs with auxiliary lemmas to simulate strong induction effects and cover all necessary cases. This method, though not as straightforward as having a native strong induction mechanism, has proved reliable through extensive testing in various recursive functions.