Compiling mutually inductive declarations

Dealing with inhomogeneous indices

Example

inductive th := t0, t1, t2
open th

mutual_inductive foo, bar, rig (A : Type)
with foo : nat → nat → Type
| mk : bar t0 → rig → foo 2 2
with bar : th → Type
| mk : rig → foo 1 1 → bar t2
with rig : Type
| mk : foo 0 0 → bar t1 → rig

We can compile this mutually inductive declaration as follows:

infixr ⊎ := sum

definition I₁ := Σ (n₁ n₂ : nat), unit
definition I₂ := Σ (t : th), unit
definition I₃ := unit

definition mk₁ (n₁ n₂ : nat) : I₁ := sigma.mk n₁ (sigma.mk n₂ unit.star)
definition mk₂ (t : th)      : I₂ := sigma.mk t unit.star
definition mk₃               : I₃ := unit.star

definition I := I₁ ⊎ (I₂ ⊎ I₃)

definition put₁ (p : I₁) : I := sum.inl p
definition put₂ (p : I₂) : I := sum.inr (sum.inl p)
definition put₃ (p : I₃) : I := sum.inr (sum.inr p)

inductive FBR (A : Type) : I → Type :=
| fmk : FBR A (put₂ $ mk₂ t0)  → FBR A (put₃ $ mk₃)      → FBR A (put₁ $ mk₁ 2 2)
| bmk : FBR A (put₃ $ mk₃)     → FBR A (put₁ $ mk₁ 1 1)  → FBR A (put₂ $ mk₂ t2)
| rmk : FBR A (put₁ $ mk₁ 0 0) → FBR A (put₂ $ mk₂ t1)   → FBR A (put₃ $ mk₃)

definition foo (A : Type) (n₁ n₂ : nat) := FBR A (put₁ $ mk₁ n₁ n₂)
definition bar (A : Type) (t : th)      := FBR A (put₂ $ mk₂ t)
definition rig (A : Type)               := FBR A (put₃ $ mk₃)

definition foo.mk (A : Type) := @FBR.fmk A
definition bar.mk (A : Type) := @FBR.bmk A
definition rig.mk (A : Type) := @FBR.rmk A

definition foo.cases_on {A : Type}
                        {C : Π {n₁ n₂ : nat}, foo A n₁ n₂ → Type}
                        {n₁ n₂ : nat}
                        (f : foo A n₁ n₂)
                        (mp : Π (b : bar A t0) (r : rig A), C (foo.mk A b r)) :=
@FBR.cases_on A
              (λ (i : I) (x : FBR A i),
                match i, x : Π (i : I), FBR A i → Type with
                | ⌞put₁⌟ (⌞mk₁⌟ n₁ n₂), f := C f
                | _,     _   := poly_unit
                end)
              (put₁ (mk₁ n₁ n₂))
              f
              mp
              (λ (r : rig A) (f : foo A 1 1), poly_unit.star)
              (λ (f : foo A 0 0) (b : bar A t1), poly_unit.star)