{n : nat} (x : nat) (h : x.+1 < n.+1) : succ_finnat (x; leq_pred' h) = (x.+1; h). Proof. by apply path_sigma_hprop. Defined.
Require Import Basics.Overture Basics.Tactics Basics.Trunc Basics.PathGroupoids Require Import Types.Empty Types.Sigma Types.Sum Types.Prod Types.Equiv. Require Import Spaces.Nat.Core. Require Import Finite.Fin.