Induction works for all types with eliminators now (some eliminators
still need fixing) including those with indicies.