{n : nat}: trunc_index_add n n = n.+1 + n.+1. Proof. induction n as [|n IHn]. 1: reflexivity. lhs nrapply trunc_index_add_succ. rhs nrapply (ap nat_to_trunc_index). 2: nrapply nat_add_succ_r. exact (ap (fun x => x.+2%trunc) IHn). Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids