fact: Fixpoint trunc_index_leq@{} (m n : trunc_index) : Type0 := match m, n with | -2, _ => Unit | m'.+1, -2 => Empty | m'.+1, n'.+1 => trunc_index_leq m' n' end.
imports: Basics.Overture Basics.Contractible Basics.Equivalences Basics.Tactics Basics.Nat