proposition: Lemma compute_finnat_ind_succ (P : forall n : nat, FinNat n -> Type) (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: Proof. refine (_ @ transport (fun p => transport _ p (s n u _) = s n u (finnat_ind P z s u)) (hset_path2 1 (path_succ_finnat u (leq_S_n' _ _ u.2))) 1). destruct u as [u1 u2]. assert (u2 = leq_S_n u1.+1 n (leq_S_n' u1.+1 n u2)) as p. - apply path_ishprop. - simpl. by induction p. Defined.
imports: HoTT.Basics HoTT.Types HoTT.HSet HoTT.Spaces.Nat.Core HoTT.Spaces.Finite.Fin