trunc_index_leq_succ'@{} n m : n <= m -> n <= m.+1. Proof. revert m. induction n as [|n IHn] using trunc_index_ind. 1: exact _. intros m p; cbn. induction m as [|m IHm] using trunc_index_ind. 1: destruct p. apply IHn, p. Defined.
Require Import