finnat_ind_beta_succ@{u} (P : forall n : nat, FinNat n -> Type@{u}) (z : forall n : nat, P n.+1 (zero_finnat n)) (s : forall (n : nat) (u : FinNat n), P n u -> P n.+1 (succ_finnat u)) {n : nat} (u : FinNat n) : finnat_ind P z s (succ_finnat u) = s n u (finnat_ind P z s u). Proof. destruct u as [u1 u2]; simpl; unfold path_succ_finnat. destruct (path_ishprop u2 (leq_pred' (leq_succ u2))). refine (transport2 _ (q:=idpath@{Set}) _ _). rapply path_ishprop. 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.