trunc_index_inc_agree@{} (k : trunc_index) (n : nat) : trunc_index_inc k n = trunc_index_inc' k n. Proof. simple_induction n n IHn. - reflexivity. - simpl. refine (ap _ IHn @ _). symmetry; apply trunc_index_inc'_succ. Defined.
Require Import