trunc_index_inc'_succ@{} (n : nat) (k : trunc_index) : trunc_index_inc' k.+1 n = (trunc_index_inc' k n).+1. Proof. revert k; simple_induction n n IHn; intro k. - reflexivity. - apply (IHn k.+1). Defined.
Require Import