trunc_index_min_path@{} n m : (trunc_index_min n m = n) + (trunc_index_min n m = m). Proof. revert m; simple_induction n n IHn; intro m. 1: by apply inl. simple_induction m m IHm. 1: by apply inr. destruct (IHn m). 1: apply inl. 2: apply inr. 1,2: cbn; by apply ap. Defined.
Require Import