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 → Type
| mk : bar t0 → rig → foo 2
with bar : th → Type
| mk : rig → foo 1 → bar t2
with rig : Type
| mk : foo 0 → bar t1 → rig

We can compile this mutually inductive declaration as follows:

infixr ⊎ := sum

definition I := (Σ (n : nat), unit) ⊎ ((Σ (t : th), unit) ⊎ unit)
definition in1 (n : ℕ) : I := sum.inl (sigma.mk n unit.star)
definition in2 (t : th) : I := sum.inr (sum.inl (sigma.mk t unit.star))
definition in3 : I := sum.inr (sum.inr unit.star)

inductive FBR (A : Type) : I → Type :=
| fmk : FBR A (in2 t0) → FBR A in3      → FBR A (in1 2)
| bmk : FBR A in3      → FBR A (in1 1)  → FBR A (in2 t2)
| rmk : FBR A (in1 0)  → FBR A (in2 t1) → FBR A in3

definition foo (A : Type) (n : nat) := FBR A (in1 n)
definition bar (A : Type) (t : th)  := FBR A (in2 t)
definition rig (A : Type)           := FBR A in3

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 : nat}, foo A n → Type}
                        {n : nat}
                        (f : foo A 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
                | ⌞in1⌟ n, f := C f
                | _,     _   := poly_unit
                end)
              (in1 n)
              f
              mp
              (λ (r : rig A) (f : foo A 1), poly_unit.star)
              (λ (f : foo A 0) (b : bar A t1), poly_unit.star)