equiv_N_segment_succ_inv_inl@{} (n : N) (mh : {m:N & m <= n}) : ((equiv_N_segment_succ n)^-1 (inl mh)).1 = mh.1. Proof. reflexivity. Qed.
Require Import Basics. Require Import Types. Require Import HProp. Require Import Universes.Smallness.