fact: Fixpoint trunc_index_inc'@{} (k : trunc_index) (n : nat) : trunc_index := match n with | O => k | S m => (trunc_index_inc' k.+1 m) end.
imports: Basics.Overture Basics.Contractible Basics.Equivalences Basics.Tactics Basics.Nat