trunc_index_add_succ@{} m n : m +2+ n.+1 = (m +2+ n).+1. Proof. revert m; simple_induction n n IHn; intro m; simple_induction m m IHm. 1,3: reflexivity. all: cbn; apply ap. all: assumption. Defined.
Require Import