Consider a set of N mutually inductive types (say N = 6) and a definition/proof by mutual recursion/induction (using `Fixpoint... with...with`

, not a mutual induction scheme). Can the definition be represented internally without N-way duplication, and does this multiply typechecking costs by N times? Is this another argument for using induction principles for such proofs?

I ask because I don't see how to avoid it, by looking at Gallina terms: While I write the recursive definition/proof once, there doesn't seem to be a way to _represent it_ in-kernel once — with actual fixpoints, I must replicate the body N times, and in each copy I must select a different member — from `fix a1 ... with aN for a1`

to `fix a1 ... with aN for an`

.

Last updated: Jan 28 2023 at 08:02 UTC