It should in particular also apply to maps (which we should clarify if they are finite!) and sets.
The benefit is that we can use induction whenever the solvers are not behaving like we want (performance or limitations of their first-order axiomatization).
Collections should be backed by lists or similar structures.
Example of some discussion of this for arrays: https://github.com/epfl-lara/stainless/issues/1281
It should in particular also apply to maps (which we should clarify if they are finite!) and sets.
The benefit is that we can use induction whenever the solvers are not behaving like we want (performance or limitations of their first-order axiomatization).